Deploy binary file

.gitmodules

@@ -10,3 +10,6 @@
 [submodule "src/tests/integration/data/contracts/test-foundry-simple/lib/kontrol-cheatcodes"]
 	path = src/tests/integration/data/contracts/test-foundry-simple/lib/kontrol-cheatcodes
 	url = https://github.com/runtimeverification/kontrol-cheatcodes
+[submodule "src/tests/integration/data/contracts/test-stylus-from-foundry/lib/forge-std"]
+	path = src/tests/integration/data/contracts/test-stylus-from-foundry/lib/forge-std
+	url = https://github.com/foundry-rs/forge-std

package/version

@@ -1 +1 @@
-0.1.19
+0.1.20

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "hatchling.build"
 
 [project]
 name = "skribe"
-version = "0.1.19"
+version = "0.1.20"
 description = "Property testing for Stylus smart contracts"
 readme = "README.md"
 requires-python = "~=3.10"

src/skribe/__main__.py

@@ -1,12 +1,10 @@
 from __future__ import annotations
 
-import json
 import sys
 from argparse import ArgumentParser
 from pathlib import Path
 
 from pyk.cli.utils import ensure_dir_path
-from pyk.utils import abs_or_rel_to
 from rich.console import Console
 
 from .skribe import InitializationError, Skribe
@@ -28,12 +26,9 @@ def _exec_build(dir_path: Path | None) -> None:
     """
     dir_path = Path.cwd() if dir_path is None else dir_path
 
-    skribe = Skribe(concrete_definition)
+    skribe = Skribe(concrete_definition, dir_path)
 
-    if (dir_path / 'foundry.toml').exists():
-        skribe.build_foundry_contract(contract_dir=dir_path)
-    else:
-        skribe.build_stylus_contract(contract_dir=dir_path)
+    skribe.build_contract()
 
     exit(0)
 
@@ -58,12 +53,10 @@ def _exec_run(dir_path: Path | None, id: str | None, max_examples: int) -> None:
 
     dir_path = Path.cwd() if dir_path is None else dir_path
 
-    skribe = Skribe(concrete_definition)
-
-    child_wasms = _read_config_file(skribe, dir_path)
+    skribe = Skribe(concrete_definition, dir_path)
 
     try:
-        failed = skribe.deploy_and_run(contract_dir=dir_path, child_wasms=child_wasms, id=id, max_examples=max_examples)
+        failed = skribe.deploy_and_run(id=id, max_examples=max_examples)
     except InitializationError:
         err_console.print('[bold red]Initialization failed[/bold red]')
         exit(1)
@@ -79,23 +72,6 @@ def _exec_run(dir_path: Path | None, id: str | None, max_examples: int) -> None:
     exit(1)
 
 
-def _read_config_file(skribe: Skribe, dir_path: Path | None = None) -> tuple[Path, ...]:
-    dir_path = Path.cwd() if dir_path is None else dir_path
-    config_path = dir_path / 'skribe.json'
-
-    def get_wasm_path(c: Path) -> Path:
-        c = abs_or_rel_to(c, dir_path)
-        assert c.is_file() and c.suffix == '.wasm'
-        return c
-
-    if config_path.is_file():
-        with open(config_path) as f:
-            config = json.load(f)
-            return tuple(get_wasm_path(Path(c)) for c in config['contracts'])
-
-    return ()
-
-
 def _argument_parser() -> ArgumentParser:
     parser = ArgumentParser(prog='skribe')
     command_parser = parser.add_subparsers(dest='command', required=True)

src/skribe/kast/syntax.py

@@ -56,3 +56,7 @@ def check_foundry_success() -> KInner:
 
 def check_output(bs: bytes) -> KInner:
     return KApply('checkOutput', [token(bs)])
+
+
+def pyk_hook_result(sig: str, k: KInner) -> KInner:
+    return KApply('skribe.pykHookResult', [token(sig), k])

src/skribe/kdist/stylus-semantics/configuration.md

@@ -29,6 +29,7 @@ module CONFIGURATION
           </stylusvm>
         </stylusvms>
         <foundry/>
+        <parsedWasmCache> .Map </parsedWasmCache> // ACCTID:Int |-> WASMMOD:ModuleDecl
       </stylus>
 
     syntax StylusStack ::= List{StylusStackVal, ":"}  [symbol(stylusStackList)]
@@ -97,14 +98,6 @@ These internal commands manages the call stack when calling and returning from a
         (_:CallStateCell => CALLSTATE)
         (_:StylusvmsCell => <stylusvms> STYLUSVM </stylusvms>)
 
-    syntax InternalCmd ::= "#resetCallState"
- // ---------------------------------------
-    rule [resetCallState]:
-        <k> #resetCallState => .K ... </k>
-        (_:CallStateCell => <callState> <program> .Bytes </program> ... </callState>)
-        (_:StylusvmsCell => <stylusvms> .Bag </stylusvms>)
-      [preserves-definedness] // all constant configuration cells should be defined
-
 ```
 
 ```k

src/skribe/kdist/stylus-semantics/hostfuns.md

@@ -235,6 +235,44 @@ Equivalent to the [`SLOAD`](https://www.evm.codes/#54) opcode in EVM.
 
 ```
 
+## static_call_contract
+
+```k
+    rule [hostCall-static-call-contract]:
+        <instrs> hostCall ( "vm_hooks" , "static_call_contract" , [ i32  i32  i32  i64  i32  .ValTypes ] -> [ i32  .ValTypes ] )
+              => pushStack(RET_LEN_PTR)
+              ~> #memLoad(DATA_PTR, DATA_LEN)
+              ~> #memLoad(CONTRACT_PTR, 20)
+              ~> #asWordFromStack
+              ~> hostCallAux("vm_hooks", "static_call_contract")
+                 ...
+        </instrs>
+        <locals>
+          0 |-> < i32 > CONTRACT_PTR
+          1 |-> < i32 > DATA_PTR
+          2 |-> < i32 > DATA_LEN
+          3 |-> < i64 > _GAS
+          4 |-> < i32 > RET_LEN_PTR
+        </locals>
+        <k> #endWasm ... </k>
+
+    rule [hostCallAux-static-call-contract]:
+        <instrs> hostCallAux ( "vm_hooks" , "static_call_contract" )
+              => #waitCommands
+                 ...
+        </instrs>
+        <k> (.K => #accessAccounts ACCTTO
+                ~> #checkCall ACCTFROM 0
+                ~> #call ACCTFROM ACCTTO ACCTTO 0 0 DATA false
+                ~> #returnStylus RET_LEN_PTR
+            ) 
+          ~> #endWasm ... 
+        </k>
+        <stylusStack> ACCTTO : (DATA : RET_LEN_PTR : S) => S </stylusStack>
+        <id> ACCTFROM </id>
+
+```
+
 ## read_return_data
 
 ```k
@@ -256,6 +294,64 @@ Equivalent to the [`SLOAD`](https://www.evm.codes/#54) opcode in EVM.
         <output> OUTPUT </output>
         <k> #endWasm ... </k>
 
+
+```
+
+## create1
+
+```k
+    rule [hostCall-create1]:
+        <instrs> hostCall ( "vm_hooks" , "create1" , [ i32  i32  i32  i32  i32  .ValTypes ] -> [ .ValTypes ] )
+              => pushStack(REVERT_LEN_PTR)
+              ~> pushStack(CONTRACT_PTR)
+              ~> #memLoad(ENDOWMENT_PTR, 32)
+              ~> #asWordFromStack
+              ~> #memLoad(CODE_PTR, CODE_LEN)
+              ~> hostCallAux("vm_hooks", "create1")
+                 ...
+        </instrs>
+        <locals>
+          0 |-> < i32 > CODE_PTR
+          1 |-> < i32 > CODE_LEN
+          2 |-> < i32 > ENDOWMENT_PTR
+          3 |-> < i32 > CONTRACT_PTR
+          4 |-> < i32 > REVERT_LEN_PTR
+        </locals>
+        <k> #endWasm ... </k>
+
+    // TODO check valid init code
+    rule [hostCallAux-create1]:
+        <instrs> hostCallAux ( "vm_hooks" , "create1" )
+              => #waitCommands
+              ~> #returnCreateResult CONTRACT_PTR REVERT_LEN_PTR
+                 ...
+        </instrs>
+        <k> (.K => #accessAccounts #newAddr(ACCT, NONCE)
+                ~> #checkCreate ACCT ENDOWMENT
+                ~> #create ACCT #newAddr(ACCT, NONCE) ENDOWMENT CODE
+                ~> #codeDeposit #newAddr(ACCT, NONCE)
+            )
+            ~> #endWasm ...
+        </k>
+        <id> ACCT </id>
+        <account>
+          <acctID> ACCT </acctID>
+          <nonce> NONCE </nonce>
+          ...
+        </account>
+        <stylusStack> CODE:Bytes : ENDOWMENT:Int : CONTRACT_PTR:Int : REVERT_LEN_PTR:Int : S => S </stylusStack>
+
+    syntax InternalInstr ::= "#returnCreateResult" Int Int
+ // ----------------------------------------------
+    rule [returnCreateResult]:
+        <instrs> #returnCreateResult CONTRACT_PTR REVERT_LEN_PTR
+              => #memStore(REVERT_LEN_PTR, Int2Bytes(32, lengthBytes(OUT), BE))
+              ~> #memStore(CONTRACT_PTR, Int2Bytes(20, ADDR, BE))
+                 ...
+        </instrs>
+        <wordStack> ADDR : S => S </wordStack>
+        <output> OUT </output>
+
 ```
 
 ```k

src/skribe/kdist/stylus-semantics/memory-opt.md

@@ -0,0 +1,41 @@
+
+`SparseBytes` represents Wasm memory as a sequence of chunks, each either an empty region (`#empty(N)`) or a block of
+concrete bytes (`#bytes(B)`). Under programs with many small writes, this structure can become heavily fragmented: long
+runs of tiny adjacent chunks appear, inflating the configuration and slowing down memory operations.
+
+To mitigate this, a simple post-write optimization is added. After every store (via `#setBytesRange`), the result of 
+`replaceAt` is passed through a compaction function that merges consecutive chunks:
+* `#empty(N)` followed by `#empty(M)` becomes `#empty(N + M)`.
+* `#bytes(B1)` followed by `#bytes(B2)` becomes `#bytes(B1 + B2)`.
+
+This preserves the semantics of memory while keeping the `SparseBytes` structure compact, reducing fragmentation and
+improving performance in workloads with frequent small writes.
+
+```k
+// TODO upstream this optimization
+
+requires "wasm-semantics/wasm-data.md"
+
+module WASM-MEMORY-OPT
+    imports WASM-DATA
+
+    rule #setBytesRange(BM, START, BS)
+      => compactSparseBytes(replaceAt(BM, START, BS))
+      [priority(30)]
+
+    syntax SparseBytes ::= compactSparseBytes(SparseBytes) [function, total]
+
+    // merge empty sections
+    rule compactSparseBytes(SBChunk(#empty(N)) SBChunk(#empty(M)) REST)
+      => compactSparseBytes(SBChunk(#empty(N +Int M)) REST)
+
+    // merge consecutive byte sections
+    rule compactSparseBytes(SBChunk(#bytes(B1)) SBChunk(#bytes(B2)) REST)
+      => compactSparseBytes(SBChunk(#bytes(B1 +Bytes B2)) REST)
+
+    // skip otherwise
+    rule compactSparseBytes(S:SBItemChunk REST) => S compactSparseBytes(REST)         [owise]
+    rule compactSparseBytes(.SparseBytes)       => .SparseBytes                       [owise]
+
+endmodule
+```

src/skribe/kdist/stylus-semantics/skribe.md

@@ -32,6 +32,7 @@ module SKRIBE
     imports STYLUS
     imports SKRIBE-SYNTAX-COMMON
     imports SKRIBE-ASSUME-CONCRETE
+    imports SKRIBE-CHEAT-CODES
 
     rule [steps-empty]:
         <k> .Steps => .K </k>
@@ -125,6 +126,33 @@ module SKRIBE
         <k> #halt => #popCallStack ~> #dropWorldState </k>
         <stylusvms> .Bag </stylusvms>
 
+```
+
+### Cheatcode calling mechanism for Skribe
+
+```k
+    syntax KItem ::= "#cheatcode_returnStylus" Int  [symbol(cheatcode_returnStylus)]
+
+    rule [cheatcode.call.stylus]:
+        <k> (#checkCall _ _
+        ~> #call _ CHEAT_ADDR _ _ _ ARGS _
+        ~> #returnStylus RET_LEN_PTR )
+        => #cheatcode_call #asWord(#range(ARGS, 0, 4)) #range(ARGS, 4, lengthBytes(ARGS) -Int 4)
+        ~> #cheatcode_returnStylus RET_LEN_PTR
+        ...
+        </k>
+        <output> _ => .Bytes </output>
+      requires CHEAT_ADDR ==Int #address(FoundryCheat)
+      [priority(40)]
+
+    rule [cheatcode.return]:
+        <k> #cheatcode_returnStylus RET_LEN_PTR => .K ... </k>
+        <instrs> (.K => #memStore(RET_LEN_PTR, Int2Bytes(4, lengthBytes(OUT), LE))
+                     ~> i32.const 0) 
+                  ...
+        </instrs>
+        <output> OUT </output>
+
 endmodule
 ```
 
@@ -151,3 +179,41 @@ module SKRIBE-ASSUME-CONCRETE [concrete]
 
 endmodule
 ```
+
+### Pyk Hooks for Cheatcodes
+
+```k
+module SKRIBE-CHEAT-CODES
+    imports STYLUS
+    imports SKRIBE-SYNTAX-COMMON
+
+    rule selector ( "readFileBinary(string)" ) => 384662468
+
+    rule [skribe.cheatcode.call.readFile]:
+        <k> #cheatcode_call SELECTOR ARGS
+         => #pykHook "readFile(string)" ARGS
+            ...
+        </k>
+      requires SELECTOR ==Int selector( "readFile(string)" )
+
+    rule [skribe.pykHookResult.readFile]:
+        <k> #pykHookResult "readFile(string)" ABI_ENCODED_CONTENT
+         => .K ...
+        </k>
+        <output> _ => ABI_ENCODED_CONTENT </output>
+
+    rule [skribe.cheatcode.call.readFileBinary]:
+        <k> #cheatcode_call SELECTOR ARGS
+         => #pykHook "readFileBinary(string)" ARGS
+            ...
+        </k>
+      requires SELECTOR ==Int selector( "readFileBinary(string)" )
+
+    rule [skribe.pykHookResult.readFileBinary]:
+        <k> #pykHookResult "readFileBinary(string)" ABI_ENCODED_CONTENT
+         => .K ...
+        </k>
+        <output> _ => ABI_ENCODED_CONTENT </output>
+
+endmodule
+```