From 3b9a1d913f68ed1ace9414515852eac3276f798f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Burak=20Bilge=20Yal=C3=A7=C4=B1nkaya?= Date: Mon, 18 Nov 2024 11:28:21 +0300 Subject: [PATCH 1/3] Implement `symbol_index_in_linear_memory` (#46) * move `loadSlices` to `symbol.md` * implement `symbol_index_in_linear_memory` * add komet test * Set Version: 0.1.39 * Set Version: 0.1.40 --------- Co-authored-by: devops --- package/version | 2 +- pyproject.toml | 2 +- src/komet/kdist/soroban-semantics/host/map.md | 42 -------- .../kdist/soroban-semantics/host/symbol.md | 99 ++++++++++++++++++- .../contracts/test_custom_types/Cargo.toml | 15 +++ .../contracts/test_custom_types/src/lib.rs | 50 ++++++++++ 6 files changed, 165 insertions(+), 45 deletions(-) create mode 100644 src/tests/integration/data/soroban/contracts/test_custom_types/Cargo.toml create mode 100644 src/tests/integration/data/soroban/contracts/test_custom_types/src/lib.rs diff --git a/package/version b/package/version index 528bd040..7172442a 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.39 +0.1.40 diff --git a/pyproject.toml b/pyproject.toml index 2ddbf918..a2eab2ac 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "komet" -version = "0.1.39" +version = "0.1.40" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", diff --git a/src/komet/kdist/soroban-semantics/host/map.md b/src/komet/kdist/soroban-semantics/host/map.md index aef32caf..9e6adfd4 100644 --- a/src/komet/kdist/soroban-semantics/host/map.md +++ b/src/komet/kdist/soroban-semantics/host/map.md @@ -102,47 +102,5 @@ The function returns a `HostVal` pointing to the new map object. RELS requires size(KEYS) ==Int lengthBytes(VALS_BS) /Int 8 -``` - -## Helpers - - -```k - - syntax List ::= Bytes2U32List(Bytes) [function, total, symbol(Bytes2U32List)] - // -------------------------------------------------------------------------------- - rule Bytes2U32List(BS) => ListItem(Bytes2Int(substrBytes(BS, 0, 4), LE, Unsigned)) - Bytes2U32List(substrBytes(BS, 4, lengthBytes(BS))) - requires lengthBytes(BS) >=Int 4 - rule Bytes2U32List(BS) => .List - requires lengthBytes(BS) loadSlices - => loadSlicesAux(Bytes2U32List(KEY_SLICES)) - ~> collectStackObjects(lengthBytes(KEY_SLICES) /Int 8) - ... - - KEY_SLICES : S => S - - rule [loadSlicesAux-empty]: - loadSlicesAux(.List) => .K ... - - rule [loadSlicesAux]: - loadSlicesAux(REST ListItem(OFFSET) ListItem(LEN)) - => #memLoad(OFFSET, LEN) - ~> mkSymbolFromStack - ~> loadSlicesAux(REST) - ... - - endmodule ``` \ No newline at end of file diff --git a/src/komet/kdist/soroban-semantics/host/symbol.md b/src/komet/kdist/soroban-semantics/host/symbol.md index 61032ec1..1ea94b99 100644 --- a/src/komet/kdist/soroban-semantics/host/symbol.md +++ b/src/komet/kdist/soroban-semantics/host/symbol.md @@ -11,8 +11,11 @@ module HOST-SYMBOL imports WASM-OPERATIONS imports HOST-INTEGER imports SWITCH-SYNTAX +``` - // symbol_new_from_linear_memory +## symbol_new_from_linear_memory + +```k rule [hostfun-symbol-new-from-linear-memory]: hostCall ( "b" , "j" , [ i64 i64 .ValTypes ] -> [ i64 .ValTypes ] ) => #memLoad(getMajor(HostVal(LM_POS)), getMajor(HostVal(LEN))) @@ -38,11 +41,105 @@ module HOST-SYMBOL BS:Bytes : S => S requires validSymbol(Bytes2String(BS)) + // TODO add validity check syntax InternalInstr ::= "mkSymbolFromStack" [symbol(mkSymbolFromStack)] // --------------------------------------------------------------------------------- rule [mkSymbolFromStack]: mkSymbolFromStack => .K ... (BS => Symbol(Bytes2String(BS))) : _ +``` + +## symbol_index_in_linear_memory + +Linear search a `Symbol` in an array of byte slices. Return the index of the element or trap if not found. + +```k + rule [hostfun-symbol-index-in-linear-memory]: + hostCall ( "b" , "m" , [ i64 i64 i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => loadObject(HostVal(SYMBOL)) + ~> #memLoad(getMajor(HostVal(POS)), 8 *Int getMajor(HostVal(LEN))) + ~> loadSlices + ~> symbolIndexInLinearMemory + ... + + + 0 |-> < i64 > SYMBOL // Symbol + 1 |-> < i64 > POS // U32VAL + 2 |-> < i64 > LEN // U32VAL + + requires fromSmallValid(HostVal(POS)) + andBool fromSmallValid(HostVal(LEN)) + + syntax InternalInstr ::= "symbolIndexInLinearMemory" [symbol(symbolIndexInLinearMemory)] + | symbolIndexInLinearMemoryAux(Int) [symbol(symbolIndexInLinearMemoryAux)] + // ------------------------------------------------------------------------------------------------------ + rule [symbolIndexInLinearMemory]: + symbolIndexInLinearMemory + => symbolIndexInLinearMemoryAux(indexOf(HAYSTACK, NEEDLE)) + ... + + NEEDLE:List : (Symbol(_) #as HAYSTACK) : S => S + + rule [symbolIndexInLinearMemoryAux-trap]: + symbolIndexInLinearMemoryAux(-1) => trap ... + + rule [symbolIndexInLinearMemoryAux]: + symbolIndexInLinearMemoryAux(N) => toSmall(U32(N)) ... + requires N =/=Int -1 + +``` + +## Helpers + + +```k + + syntax List ::= Bytes2U32List(Bytes) [function, total, symbol(Bytes2U32List)] + // -------------------------------------------------------------------------------- + rule Bytes2U32List(BS) => ListItem(Bytes2Int(substrBytes(BS, 0, 4), LE, Unsigned)) + Bytes2U32List(substrBytes(BS, 4, lengthBytes(BS))) + requires lengthBytes(BS) >=Int 4 + rule Bytes2U32List(BS) => .List + requires lengthBytes(BS) loadSlices + => loadSlicesAux(Bytes2U32List(KEY_SLICES)) + ~> collectStackObjects(lengthBytes(KEY_SLICES) /Int 8) + ... + + KEY_SLICES : S => S + + rule [loadSlicesAux-empty]: + loadSlicesAux(.List) => .K ... + + rule [loadSlicesAux]: + loadSlicesAux(REST ListItem(OFFSET) ListItem(LEN)) + => #memLoad(OFFSET, LEN) + ~> mkSymbolFromStack + ~> loadSlicesAux(REST) + ... + +``` + +- `indexOf(X, XS)`: returns the index of the first element in `XS` which is equal to `X`, or `-1` if there is no such element. + +```k + syntax Int ::= indexOf (KItem, List) [function, total, symbol(indexOf)] + | indexOfAux(KItem, List, Int) [function, total, symbol(indexOfAux)] + // -------------------------------------------------------------------------- + rule indexOf(X, XS) => indexOfAux(X, XS, 0) + rule indexOfAux(_, .List, _) => -1 + rule indexOfAux(X, ListItem(Y) _, N) => N requires X ==K Y + rule indexOfAux(X, ListItem(Y) XS, N) => indexOfAux(X, XS, N +Int 1) requires X =/=K Y endmodule ``` \ No newline at end of file diff --git a/src/tests/integration/data/soroban/contracts/test_custom_types/Cargo.toml b/src/tests/integration/data/soroban/contracts/test_custom_types/Cargo.toml new file mode 100644 index 00000000..1cc50ccb --- /dev/null +++ b/src/tests/integration/data/soroban/contracts/test_custom_types/Cargo.toml @@ -0,0 +1,15 @@ +[package] +name = "test_custom_types" +version = "0.0.0" +edition = "2021" +publish = false + +[lib] +crate-type = ["cdylib"] +doctest = false + +[dependencies] +soroban-sdk = { workspace = true } + +[dev-dependencies] +soroban-sdk = { workspace = true, features = ["testutils"] } diff --git a/src/tests/integration/data/soroban/contracts/test_custom_types/src/lib.rs b/src/tests/integration/data/soroban/contracts/test_custom_types/src/lib.rs new file mode 100644 index 00000000..04be9a81 --- /dev/null +++ b/src/tests/integration/data/soroban/contracts/test_custom_types/src/lib.rs @@ -0,0 +1,50 @@ +#![no_std] +use soroban_sdk::{contract, contractimpl, contracttype, symbol_short, Address, Bytes, Env, FromVal, Symbol, TryFromVal, TryIntoVal, Val, Vec, EnvBase}; + +#[contract] +pub struct TestCustomTypesContract; + +#[contracttype] +#[derive(PartialEq)] +pub enum MyBool { + True, + False +} + +fn to_bool(p: &MyBool) -> bool { + match p { + MyBool::True => true, + MyBool::False => false + } +} + +fn from_bool(p: bool) -> MyBool { + if p { + MyBool::True + } else { + MyBool::False + } +} + + +#[contractimpl] +impl TestCustomTypesContract { + + pub fn test_my_bool_roundtrip(env: Env, p: bool) -> bool { + + // mp:MyBool lives in the Wasm memory + let mp = from_bool(p); + + // convert MyBool to a host object + let v: Val = mp.try_into_val(&env).unwrap(); + + // convert v:Val to MyBool, load it to the Wasm memory + // (using the 'symbol_index_in_linear_memory' host function under the hood) + let mp2: MyBool = MyBool::try_from_val(&env, &v).unwrap(); + + let p2 = to_bool(&mp2); + + mp == mp2 && p == p2 + } + +} From 50117c0354890505ed450859c2ff846524a72429 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Burak=20Bilge=20Yal=C3=A7=C4=B1nkaya?= Date: Tue, 19 Nov 2024 11:01:50 +0300 Subject: [PATCH 2/3] Implement Contract Upgrade and TTL Management Host Functions (#47) * fix `getTag(SCBool(_))` * implement `update_current_contract_wasm` and add a wast test * add live-until field to storage entries * implement `extend_contract_data_ttl` * add `storage.wast` tests * update `test_ttl` after introducing `#maxEntryTtl` * Set Version: 0.1.39 * Set Version: 0.1.41 --------- Co-authored-by: devops --- package/version | 2 +- pyproject.toml | 2 +- .../kdist/soroban-semantics/configuration.md | 12 +- src/komet/kdist/soroban-semantics/data.md | 4 +- .../kdist/soroban-semantics/host/ledger.md | 112 +++++++++++++++- .../soroban/contracts/test_ttl/src/lib.rs | 28 ++-- src/tests/integration/data/storage.wast | 121 ++++++++++++++++++ src/tests/integration/data/update_wasm.wast | 59 +++++++++ 8 files changed, 323 insertions(+), 17 deletions(-) create mode 100644 src/tests/integration/data/storage.wast create mode 100644 src/tests/integration/data/update_wasm.wast diff --git a/package/version b/package/version index 7172442a..37f868fb 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.40 +0.1.41 diff --git a/pyproject.toml b/pyproject.toml index a2eab2ac..21c083f1 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "komet" -version = "0.1.40" +version = "0.1.41" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", diff --git a/src/komet/kdist/soroban-semantics/configuration.md b/src/komet/kdist/soroban-semantics/configuration.md index 6053cba0..ed581bb6 100644 --- a/src/komet/kdist/soroban-semantics/configuration.md +++ b/src/komet/kdist/soroban-semantics/configuration.md @@ -65,7 +65,7 @@ module CONFIG Keys and values must be fully resolved `ScVal`s as in ``. ```k - .Map // Map of StorageKey to ScVal + .Map // Map of StorageKey to StorageVal .Bytes @@ -99,6 +99,8 @@ module CONFIG syntax StorageKey ::= #skey( ContractId , Durability , ScVal ) [symbol(StorageKey)] + syntax StorageVal ::= #sval( ScVal , Int ) [symbol(StorageVal)] + endmodule ``` @@ -470,6 +472,14 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly ``` +## Exception throwing + ```k + syntax InternalInstr ::= #throw(ErrorType, Int) [symbol(throw)] + // ------------------------------------------------------------------ + rule [throw]: + #throw(ERRTYPE, CODE) ~> _REST => .K + S => Error(ERRTYPE, CODE) : S + endmodule ``` \ No newline at end of file diff --git a/src/komet/kdist/soroban-semantics/data.md b/src/komet/kdist/soroban-semantics/data.md index ea1a64b7..b33b5c68 100644 --- a/src/komet/kdist/soroban-semantics/data.md +++ b/src/komet/kdist/soroban-semantics/data.md @@ -143,8 +143,8 @@ module HOST-OBJECT // https://github.com/stellar/stellar-protocol/blob/master/core/cap-0046-01.md#tag-values syntax Int ::= getTag(ScVal) [function, total] // ----------------------------------------------------- - rule getTag(SCBool(true)) => 0 - rule getTag(SCBool(false)) => 1 + rule getTag(SCBool(false)) => 0 + rule getTag(SCBool(true)) => 1 rule getTag(Void) => 2 rule getTag(Error(_,_)) => 3 rule getTag(U32(_)) => 4 diff --git a/src/komet/kdist/soroban-semantics/host/ledger.md b/src/komet/kdist/soroban-semantics/host/ledger.md index c22cca8f..1e635dd0 100644 --- a/src/komet/kdist/soroban-semantics/host/ledger.md +++ b/src/komet/kdist/soroban-semantics/host/ledger.md @@ -37,14 +37,26 @@ module HOST-LEDGER ... - rule [putContractData-other]: + rule [putContractData-other-existing]: putContractData(DUR:Durability) => toSmall(Void) ... KEY : VAL : S => S CONTRACT - STORAGE => STORAGE [ #skey(CONTRACT, DUR, KEY) <- VAL ] + ... + #skey(CONTRACT, DUR, KEY) |-> #sval(_ => VAL, _LIVE_UNTIL) + ... + rule [putContractData-other-new]: + putContractData(DUR:Durability) => toSmall(Void) ... + KEY : VAL : S => S + CONTRACT + + STORAGE => STORAGE [ #skey(CONTRACT, DUR, KEY) <- #sval(VAL, minLiveUntil(DUR, SEQ)) ] + + SEQ + requires notBool( #skey(CONTRACT, DUR, KEY) in_keys(STORAGE) ) + ``` ## has_contract_data @@ -126,7 +138,7 @@ module HOST-LEDGER KEY : S => S CONTRACT - ... #skey(CONTRACT, DUR, KEY) |-> VAL ... + ... #skey(CONTRACT, DUR, KEY) |-> #sval(VAL, _) ... ``` @@ -165,6 +177,83 @@ module HOST-LEDGER MAP => MAP [#skey(CONTRACT, DUR, KEY) <- undef ] requires #skey(CONTRACT, DUR, KEY) in_keys(MAP) +``` +## update_current_contract_wasm + +```k + rule [hostfun-update-current-contract-wasm]: + hostCall ( "l" , "6" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => loadObject(HostVal(HASH)) + ~> updateContractWasm(CALLEE) + ~> toSmall(Void) + ... + + + 0 |-> < i64 > HASH // Bytes + + CALLEE + + syntax InternalInstr ::= updateContractWasm(ContractId) [symbol(updateContractWasm)] + // -------------------------------------------------------------------------------------- + rule [updateContractWasm]: + updateContractWasm(CONTRACT) => .K ... + ScBytes(HASH) : S => S + + CONTRACT + _ => HASH + ... + + + HASH + ... + + +``` + +## extend_contract_data_ttl + +```k + rule [hostfun-extend-contract-data-ttl]: + hostCall ( "l" , "7" , [ i64 i64 i64 i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => loadObject(HostVal(EXTEND_TO)) + ~> loadObject(HostVal(THRESHOLD)) + ~> loadObjectFull(HostVal(KEY)) + ~> extendContractDataTtl(CONTRACT, Int2StorageType(STORAGE_TYPE)) + ~> toSmall(Void) + ... + + + 0 |-> < i64 > KEY // HostVal + 1 |-> < i64 > STORAGE_TYPE // 0: temp, 1: persistent, 2: instance + 2 |-> < i64 > THRESHOLD // U32 + 3 |-> < i64 > EXTEND_TO // U32 + + CONTRACT + requires Int2StorageTypeValid(STORAGE_TYPE) + + syntax InternalInstr ::= extendContractDataTtl(ContractId, StorageType) [symbol(extendContractDataTtl)] + // -------------------------------------------------------------------------------------------- + rule [extendContractDataTtl]: + extendContractDataTtl(CONTRACT, DUR:Durability) => .K ... + KEY:ScVal : U32(THRESHOLD) : U32(EXTEND_TO) : S => S + + ... + #skey(CONTRACT, DUR, KEY) + |-> #sval(_VAL, LIVE_UNTIL => extendedLiveUntil(SEQ, LIVE_UNTIL, THRESHOLD, EXTEND_TO)) + ... + + SEQ + requires THRESHOLD <=Int EXTEND_TO // input is valid + andBool SEQ <=Int LIVE_UNTIL // entry is alive + andBool ( DUR =/=K #temporary + orBool extendedLiveUntil(SEQ, LIVE_UNTIL, THRESHOLD, EXTEND_TO) <=Int maxLiveUntil(SEQ) + ) // #temporary TTLs has to be exact + + rule [extendContractDataTtl-err]: + extendContractDataTtl(_CONTRACT, _TYP) => #throw(ErrStorage, InvalidAction) ... + _KEY:ScVal : U32(_THRESHOLD) : U32(_EXTEND_TO) : S => S + [owise] + ``` ## extend_current_contract_instance_and_code_ttl @@ -207,7 +296,8 @@ module HOST-LEDGER syntax Int ::= extendedLiveUntil(Int, Int, Int, Int) [function, total] // ----------------------------------------------------------------------------------- - rule extendedLiveUntil(SEQ, LIVE_UNTIL, THRESHOLD, EXTEND_TO) => SEQ +Int EXTEND_TO + rule extendedLiveUntil(SEQ, LIVE_UNTIL, THRESHOLD, EXTEND_TO) + => minInt( SEQ +Int EXTEND_TO , maxLiveUntil(SEQ) ) requires LIVE_UNTIL -Int SEQ <=Int THRESHOLD // CURRENT_TTL <= THRESHOLD andBool LIVE_UNTIL 0 <=Int I andBool I <=Int 2 + // make these values variable + syntax Int ::= minEntryTtl(Durability) [function, total] + | "#maxEntryTtl" [macro] + // ------------------------------------------------- + rule minEntryTtl(#temporary) => 16 + rule minEntryTtl(#persistent) => 4096 + rule #maxEntryTtl => 6312000 + + syntax Int ::= minLiveUntil(Durability, Int) [function, total] + | maxLiveUntil(Int) [function, total] + // ----------------------------------------------------------------------- + rule minLiveUntil(DUR, SEQ) => SEQ +Int minEntryTtl(DUR) -Int 1 + rule maxLiveUntil(SEQ) => SEQ +Int #maxEntryTtl -Int 1 + endmodule ``` \ No newline at end of file diff --git a/src/tests/integration/data/soroban/contracts/test_ttl/src/lib.rs b/src/tests/integration/data/soroban/contracts/test_ttl/src/lib.rs index 53a99dd4..f84665ef 100644 --- a/src/tests/integration/data/soroban/contracts/test_ttl/src/lib.rs +++ b/src/tests/integration/data/soroban/contracts/test_ttl/src/lib.rs @@ -24,25 +24,37 @@ fn set_ledger_timestamp(env: &Env, x: u64) { } } +const MAX_ENTRY_TTL: u32 = 6312000; + #[contractimpl] impl TtlContract { pub fn test_ttl( env: Env, - init_live_until: u32, + ttl: u32, seq: u32, threshold: u32, extend_to: u32 ) -> bool { - // Given: - // contract is still alive and extend_ttl inputs are valid - if seq <= init_live_until && threshold <= extend_to { - env.storage().instance().extend_ttl(0, init_live_until); - set_ledger_sequence(seq); + // Validate the input + if threshold > ttl || threshold > extend_to || ttl == 0 || extend_to == 0 { + return true; + } + + // Set the initial TTL and ledger sequence number + env.storage().instance().extend_ttl(threshold, ttl); + let init_ttl = u32::min(ttl, MAX_ENTRY_TTL); + let init_seq = env.ledger().sequence(); + let init_live_until = init_seq.checked_add(init_ttl - 1); // the sequence number at the beginning is 0 + + set_ledger_sequence(seq); - // When: - env.storage().instance().extend_ttl(threshold, extend_to); + if let Some(live_until) = init_live_until { + // If the contract is still alive extend the instance ttl + if seq <= live_until { + env.storage().instance().extend_ttl(threshold, extend_to); + } } // Since there is no getter function for the TTL value, we cannot verify diff --git a/src/tests/integration/data/storage.wast b/src/tests/integration/data/storage.wast new file mode 100644 index 00000000..090fa3bd --- /dev/null +++ b/src/tests/integration/data/storage.wast @@ -0,0 +1,121 @@ + +setExitCode(1) + +uploadWasm( b"test-wasm", +(module $soroban_increment_contract.wasm + (import "l" "_" (func $put_contract_data (param i64 i64 i64) (result i64))) + (import "l" "0" (func $has_contract_data (param i64 i64) (result i64))) + (import "l" "1" (func $get_contract_data (param i64 i64) (result i64))) + (import "l" "2" (func $del_contract_data (param i64 i64) (result i64))) + (import "l" "7" (func $extend_contract_data_ttl (param i64 i64 i64 i64) (result i64))) + + (func $storage_type (param i64) (result i64) + local.get 0 + i64.const 32 + i64.shr_u + ) + + (func $put (export "put") (param i64 i64 i64) (result i64) + (call $put_contract_data + (local.get 0) + (local.get 1) + (call $storage_type (local.get 2)) + ) + ) + + (func $has (export "has") (param i64 i64) (result i64) + (call $has_contract_data + (local.get 0) + (call $storage_type (local.get 1)) + ) + ) + + (func $get (export "get") (param i64 i64) (result i64) + (call $get_contract_data + (local.get 0) + (call $storage_type (local.get 1)) + ) + ) + + (func $del (export "del") (param i64 i64) (result i64) + (call $del_contract_data + (local.get 0) + (call $storage_type (local.get 1)) + ) + ) + + + (func $extend_ttl (export "extend_ttl") (param i64 i64 i64 i64) (result i64) + (call $extend_contract_data_ttl + (local.get 0) + (call $storage_type (local.get 1)) + (local.get 2) + (local.get 3) + ) + ) +) +) + +setAccount(Account(b"test-account"), 9876543210) + +deployContract( Account(b"test-account"), Contract(b"test-sc"), b"test-wasm" ) + +;; Test put/has/get/del +;; 1. has -> false +;; 2. put "foo" U32(123456789) temp -> void +;; 3. has "foo" temp -> true +;; 4. get "foo" temp -> U32(123456789) +;; 5. del "foo" temp -> void +;; 6. has "foo" temp -> false + +callTx( + Account(b"test-caller"), Contract(b"test-sc"), + "has", ListItem(Symbol(str("foo"))) ListItem(U32(0)), + SCBool(false) +) + +callTx( + Account(b"test-caller"), Contract(b"test-sc"), + "put", ListItem(Symbol(str("foo"))) ListItem(U32(123456789)) ListItem(U32(0)), + Void +) + +callTx( + Account(b"test-caller"), Contract(b"test-sc"), + "has", ListItem(Symbol(str("foo"))) ListItem(U32(0)), + SCBool(true) +) + +callTx( + Account(b"test-caller"), Contract(b"test-sc"), + "get", ListItem(Symbol(str("foo"))) ListItem(U32(0)), + U32(123456789) +) + +callTx( + Account(b"test-caller"), Contract(b"test-sc"), + "del", ListItem(Symbol(str("foo"))) ListItem(U32(0)), + Void +) + +callTx( + Account(b"test-caller"), Contract(b"test-sc"), + "has", ListItem(Symbol(str("foo"))) ListItem(U32(0)), + SCBool(false) +) + +;; Test extend TTL +callTx( + Account(b"test-caller"), Contract(b"test-sc"), + "put", ListItem(Symbol(str("foo"))) ListItem(U32(123456789)) ListItem(U32(0)), + Void +) + +callTx( + Account(b"test-caller"), Contract(b"test-sc"), + "extend_ttl", ListItem(Symbol(str("foo"))) ListItem(U32(0)) ListItem(U32(100)) ListItem(U32(200)), + Void +) + + +setExitCode(0) \ No newline at end of file diff --git a/src/tests/integration/data/update_wasm.wast b/src/tests/integration/data/update_wasm.wast new file mode 100644 index 00000000..a0cc4e49 --- /dev/null +++ b/src/tests/integration/data/update_wasm.wast @@ -0,0 +1,59 @@ + +setExitCode(1) + +uploadWasm( b"test-wasm", +(module + (import "l" "6" (func $update_current_contract_wasm (param i64) (result i64))) + (func $update (param i64) (result i64) + local.get 0 + call $update_current_contract_wasm) + (func $foo (result i64) + i64.const 0) ;; SCBool(false) + (export "update" (func $update)) + (export "foo" (func $foo)) +) +) + +uploadWasm( b"test-wasm-2", +(module + (import "l" "6" (func $update_current_contract_wasm (param i64) (result i64))) + (func $foo (result i64) + i64.const 1) ;; SCBool(true) + (export "foo" (func $foo)) +) +) + +setAccount(Account(b"test-account"), 9876543210) + +deployContract( + Account(b"test-account"), + Contract(b"test-sc"), + b"test-wasm" +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "foo", + .List, + SCBool(false) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "update", + ListItem(ScBytes(b"test-wasm-2")), + Void +) + + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "foo", + .List, + SCBool(true) +) + +setExitCode(0) \ No newline at end of file From f689855fd143ad44c2a4ec5bc2d7588864c8d47f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Burak=20Bilge=20Yal=C3=A7=C4=B1nkaya?= Date: Tue, 19 Nov 2024 15:29:47 +0300 Subject: [PATCH 3/3] Implement `i64` and `i128` Types and Host Functions (#45) * implement `i64` * implement `i128` * add komet tests for i128 operations * `test_adder`: add `i64` and `i128` tests * Set Version: 0.1.38 * Set Version: 0.1.39 * enable `--id` argument in `komet prove` * update `test_prove_adder` to use `--id` argument to skip new properties * Set Version: 0.1.42 --------- Co-authored-by: devops --- package/version | 2 +- pyproject.toml | 2 +- src/komet/kasmer.py | 7 +- src/komet/kdist/soroban-semantics/data.md | 33 +++- .../kdist/soroban-semantics/host/integer.md | 57 +++++++ src/komet/komet.py | 8 +- src/tests/integration/data/i128.wast | 150 ++++++++++++++++++ src/tests/integration/data/i64.wast | 66 ++++++++ .../soroban/contracts/test_adder/src/lib.rs | 26 +++ .../contracts/test_integers/Cargo.toml | 15 ++ .../soroban/contracts/test_integers/README.md | 18 +++ .../contracts/test_integers/src/lib.rs | 53 +++++++ src/tests/integration/test_integration.py | 2 +- 13 files changed, 429 insertions(+), 10 deletions(-) create mode 100644 src/tests/integration/data/i128.wast create mode 100644 src/tests/integration/data/i64.wast create mode 100644 src/tests/integration/data/soroban/contracts/test_integers/Cargo.toml create mode 100644 src/tests/integration/data/soroban/contracts/test_integers/README.md create mode 100644 src/tests/integration/data/soroban/contracts/test_integers/src/lib.rs diff --git a/package/version b/package/version index 37f868fb..4a3e97d0 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.41 +0.1.42 diff --git a/pyproject.toml b/pyproject.toml index 21c083f1..f1879430 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "komet" -version = "0.1.41" +version = "0.1.42" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", diff --git a/src/komet/kasmer.py b/src/komet/kasmer.py index 0507724f..a33617b7 100644 --- a/src/komet/kasmer.py +++ b/src/komet/kasmer.py @@ -270,6 +270,7 @@ def deploy_and_prove( self, contract_wasm: Path, child_wasms: tuple[Path, ...], + id: str | None = None, proof_dir: Path | None = None, bug_report: BugReport | None = None, ) -> None: @@ -290,9 +291,9 @@ def deploy_and_prove( conf, subst = self.deploy_test(contract_kast, child_kasts, has_init) - for binding in bindings: - if not binding.name.startswith('test_'): - continue + test_bindings = [b for b in bindings if b.name.startswith('test_') and (id is None or b.name == id)] + + for binding in test_bindings: proof = self.run_prove(conf, subst, binding, proof_dir, bug_report) if proof.status == ProofStatus.FAILED: raise KSorobanError(proof.summary) diff --git a/src/komet/kdist/soroban-semantics/data.md b/src/komet/kdist/soroban-semantics/data.md index b33b5c68..1df7297a 100644 --- a/src/komet/kdist/soroban-semantics/data.md +++ b/src/komet/kdist/soroban-semantics/data.md @@ -59,6 +59,7 @@ various contexts: | U64(Int) [symbol(SCVal:U64)] | I64(Int) [symbol(SCVal:I64)] | U128(Int) [symbol(SCVal:U128)] + | I128(Int) [symbol(SCVal:I128)] | ScVec(List) [symbol(SCVal:Vec)] // List | ScMap(Map) [symbol(SCVal:Map)] // Map | ScAddress(Address) [symbol(SCVal:Address)] @@ -151,9 +152,12 @@ module HOST-OBJECT rule getTag(I32(_)) => 5 rule getTag(U64(I)) => 6 requires I <=Int #maxU64small rule getTag(U64(I)) => 64 requires notBool( I <=Int #maxU64small ) - rule getTag(I64(_)) => 65 // I64small is not implemented + rule getTag(I64(I)) => 7 requires #minI64small <=Int I andBool I <=Int #maxI64small + rule getTag(I64(I)) => 65 requires notBool( #minI64small <=Int I andBool I <=Int #maxI64small ) rule getTag(U128(I)) => 10 requires I <=Int #maxU64small rule getTag(U128(I)) => 68 requires notBool( I <=Int #maxU64small ) // U64small and U128small have the same width + rule getTag(I128(I)) => 11 requires #minI64small <=Int I andBool I <=Int #maxI64small + rule getTag(I128(I)) => 69 requires notBool( #minI64small <=Int I andBool I <=Int #maxI64small ) rule getTag(ScVec(_)) => 75 rule getTag(ScMap(_)) => 76 rule getTag(ScAddress(_)) => 77 @@ -225,8 +229,16 @@ module HOST-OBJECT rule fromSmall(VAL) => U64(getBody(VAL)) requires getTag(VAL) ==Int 6 + rule fromSmall(VAL) => I64(#signed(i56, getBody(VAL))) + requires getTag(VAL) ==Int 7 + andBool definedSigned(i56, getBody(VAL)) + rule fromSmall(VAL) => U128(getBody(VAL)) requires getTag(VAL) ==Int 10 + rule fromSmall(VAL) => I128(#signed(i56, getBody(VAL))) + requires getTag(VAL) ==Int 11 + andBool definedSigned(i56, getBody(VAL)) + rule fromSmall(VAL) => Symbol(decode6bit(getBody(VAL))) requires getTag(VAL) ==Int 14 @@ -249,7 +261,13 @@ module HOST-OBJECT rule toSmall(I32(I)) => fromMajorMinorAndTag(#unsigned(i32, I), 0, 5) requires definedUnsigned(i32, I) rule toSmall(U64(I)) => fromBodyAndTag(I, 6) requires I <=Int #maxU64small + rule toSmall(I64(I)) => fromBodyAndTag(#unsigned(i56, I), 7) + requires #minI64small <=Int I andBool I <=Int #maxI64small + andBool definedUnsigned(i56, I) rule toSmall(U128(I)) => fromBodyAndTag(I, 10) requires I <=Int #maxU64small + rule toSmall(I128(I)) => fromBodyAndTag(#unsigned(i56, I), 11) + requires #minI64small <=Int I andBool I <=Int #maxI64small + andBool definedUnsigned(i56, I) rule toSmall(Symbol(S)) => fromBodyAndTag(encode6bit(S), 14) requires lengthString(S) <=Int 9 rule toSmall(_) => HostVal(-1) [owise] @@ -307,5 +325,18 @@ module HOST-OBJECT rule tail(S) => "" requires lengthString(S) <=Int 0 rule tail(S) => substrString(S, 1, lengthString(S)) requires lengthString(S) >Int 0 + // 56-bit integers for small values + syntax IWidth ::= "i56" + // ------------------------------------ + rule #width(i56) => 56 + rule #pow(i56) => 72057594037927936 + rule #pow1(i56) => 36028797018963968 + + syntax IWidth ::= "i128" + // ------------------------------------ + rule #width(i128) => 128 + rule #pow(i128) => 340282366920938463463374607431768211456 + rule #pow1(i128) => 170141183460469231731687303715884105728 + endmodule ``` diff --git a/src/komet/kdist/soroban-semantics/host/integer.md b/src/komet/kdist/soroban-semantics/host/integer.md index de1bcb98..959b5a03 100644 --- a/src/komet/kdist/soroban-semantics/host/integer.md +++ b/src/komet/kdist/soroban-semantics/host/integer.md @@ -44,6 +44,17 @@ module HOST-INTEGER (.K => allocObject(U64(I))) ... + rule [hostfun-obj-from-i64]: + hostCall ( "i" , "1" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => allocObject(I64(#signed(i64, VAL))) + ~> returnHostVal + ... + + + 0 |-> < i64 > VAL + + requires definedSigned(i64, VAL) + rule [hostfun-obj-to-i64]: hostCall ( "i" , "2" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] ) => loadObject(HostVal(VAL)) @@ -99,5 +110,51 @@ module HOST-INTEGER U128(I) : S => S [preserves-definedness] // 'X >>Int K' is defined for positive K + rule [hostfun-obj-from-i128-pieces]: + hostCall ( "i" , "6" , [ i64 i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => allocObject(I128(#signed(i128, (HIGH < returnHostVal + ... + + + 0 |-> < i64 > HIGH + 1 |-> < i64 > LOW + + requires definedSigned(i128, (HIGH < hostCall ( "i" , "7" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => loadObject(HostVal(VAL)) + ~> i128lo64 + ... + + + 0 |-> < i64 > VAL + + + syntax InternalInstr ::= "i128lo64" [symbol(i128lo64)] + // -------------------------------------------------------- + rule [i128lo64]: + i128lo64 => i64.const (#unsigned(i128, I)) ... + I128(I) : S => S + requires definedUnsigned(i128, I) + [preserves-definedness] + + rule [hostfun-obj-to-i128-hi64]: + hostCall ( "i" , "8" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => loadObject(HostVal(VAL)) + ~> i128hi64 + ... + + + 0 |-> < i64 > VAL + + + syntax InternalInstr ::= "i128hi64" [symbol(i128hi64)] + // -------------------------------------------------------- + rule [i128hi64]: + i128hi64 => i64.const (I >>Int 64) ... + I128(I) : S => S + endmodule ``` \ No newline at end of file diff --git a/src/komet/komet.py b/src/komet/komet.py index fd1fc6dd..b00d0dc6 100644 --- a/src/komet/komet.py +++ b/src/komet/komet.py @@ -51,7 +51,7 @@ def main() -> None: elif args.command == 'prove': if args.prove_command is None or args.prove_command == 'run': wasm = Path(args.wasm.name) if args.wasm is not None else None - _exec_prove_run(wasm=wasm, proof_dir=args.proof_dir, bug_report=args.bug_report) + _exec_prove_run(wasm=wasm, id=args.id, proof_dir=args.proof_dir, bug_report=args.bug_report) if args.prove_command == 'view': assert args.proof_dir is not None _exec_prove_view(proof_dir=args.proof_dir, id=args.id) @@ -101,7 +101,9 @@ def _exec_test(*, wasm: Path | None) -> None: sys.exit(0) -def _exec_prove_run(*, wasm: Path | None, proof_dir: Path | None, bug_report: BugReport | None = None) -> None: +def _exec_prove_run( + *, wasm: Path | None, id: str | None, proof_dir: Path | None, bug_report: BugReport | None = None +) -> None: kasmer = Kasmer(symbolic_definition) child_wasms: tuple[Path, ...] = () @@ -110,7 +112,7 @@ def _exec_prove_run(*, wasm: Path | None, proof_dir: Path | None, bug_report: Bu wasm = kasmer.build_soroban_contract(Path.cwd()) child_wasms = _read_config_file() - kasmer.deploy_and_prove(wasm, child_wasms, proof_dir, bug_report) + kasmer.deploy_and_prove(wasm, child_wasms, id, proof_dir, bug_report) sys.exit(0) diff --git a/src/tests/integration/data/i128.wast b/src/tests/integration/data/i128.wast new file mode 100644 index 00000000..39676035 --- /dev/null +++ b/src/tests/integration/data/i128.wast @@ -0,0 +1,150 @@ + +setExitCode(1) + +uploadWasm( b"test-wasm", +(module $test_wasm + (import "i" "_" (func $obj_from_u64 (param i64) (result i64))) + (import "i" "1" (func $obj_from_i64 (param i64) (result i64))) + (import "i" "6" (func $obj_from_i128_pieces (param i64 i64) (result i64))) + (import "i" "7" (func $obj_to_i128_lo64 (param i64) (result i64))) + (import "i" "8" (func $obj_to_i128_hi64 (param i64) (result i64))) + (func $lo (param i64) (result i64) + local.get 0 + call $obj_to_i128_lo64 + call $obj_from_u64 + ) + (func $hi (param i64) (result i64) + local.get 0 + call $obj_to_i128_hi64 + call $obj_from_i64 + ) + (func $roundtrip (param i64) (result i64) + (call $obj_from_i128_pieces + (call $obj_to_i128_hi64 (local.get 0)) + (call $obj_to_i128_lo64 (local.get 0)) + ) + ) + (export "lo" (func $lo)) + (export "hi" (func $hi)) + (export "roundtrip" (func $roundtrip)) +)) + +setAccount(Account(b"test-account"), 9876543210) + +deployContract( + Account(b"test-account"), + Contract(b"test-sc"), + b"test-wasm" +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "lo", + ;; i128::MAX + ListItem(I128(2 ^Int 127 -Int 1)), + U64(2 ^Int 64 -Int 1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "lo", + ListItem(I128(0 -Int 2 ^Int 127)), ;; i128::MIN + U64(0) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "lo", + ListItem(I128(0)), + U64(0) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "lo", + ListItem(I128(-1)), + U64(2 ^Int 64 -Int 1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "hi", + ;; 2^127-1 (i128::MAX) + ListItem(I128(2 ^Int 127 -Int 1)), + I64(9223372036854775807) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "hi", + ListItem(I128(0 -Int 2 ^Int 127)), ;; i128::MIN + I64(0 -Int 2 ^Int 63) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "hi", + ListItem(I128(0)), + I64(0) +) + + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "hi", + ListItem(I128(-1)), + I64(-1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "hi", + ListItem(I128(-2)), + I64(-1) +) + + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtrip", + ListItem(I128(0)), + I128(0) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtrip", + ListItem(I128(170141183460469231731687303715884105727)), + I128(170141183460469231731687303715884105727) +) + + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtrip", + ListItem(I128(-1)), + I128(-1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtrip", + ListItem(I128(-170141183460469231731687303715884105727)), + I128(-170141183460469231731687303715884105727) +) + + +setExitCode(0) \ No newline at end of file diff --git a/src/tests/integration/data/i64.wast b/src/tests/integration/data/i64.wast new file mode 100644 index 00000000..78c95652 --- /dev/null +++ b/src/tests/integration/data/i64.wast @@ -0,0 +1,66 @@ + +setExitCode(1) + +uploadWasm( b"test-wasm", +(module $test_wasm + (import "i" "1" (func $obj_from_i64 (param i64) (result i64))) + (import "i" "2" (func $obj_to_i64 (param i64) (result i64))) + (func $roundtrip (param i64) (result i64) + (call $obj_from_i64 + (call $obj_to_i64 (local.get 0)) + ) + ) + (export "roundtrip" (func $roundtrip)) +)) + +setAccount(Account(b"test-account"), 9876543210) + +deployContract( + Account(b"test-account"), + Contract(b"test-sc"), + b"test-wasm" +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtrip", + ListItem(I64(1)), + I64(1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtrip", + ListItem(I64(0)), + I64(0) +) + + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtrip", + ListItem(I64(-1)), + I64(-1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtrip", + ListItem(I64(2 ^Int 63 -Int 1)), + I64(2 ^Int 63 -Int 1) +) + + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtrip", + ListItem(I64(0 -Int 2 ^Int 63)), + I64(0 -Int 2 ^Int 63) +) + +setExitCode(0) \ No newline at end of file diff --git a/src/tests/integration/data/soroban/contracts/test_adder/src/lib.rs b/src/tests/integration/data/soroban/contracts/test_adder/src/lib.rs index 45cf218e..297b52cf 100644 --- a/src/tests/integration/data/soroban/contracts/test_adder/src/lib.rs +++ b/src/tests/integration/data/soroban/contracts/test_adder/src/lib.rs @@ -10,10 +10,36 @@ impl AdderContract { first as u64 + second as u64 } + + pub fn add_i64(env: Env, first: i64, second: i64) -> i128 { + first as i128 + second as i128 + } + + pub fn increment_i128(env: Env, x: i128) -> i128 { + x + 1 + } + + ///////////////////////////////////////////////////////////////////// + /// Properties + /// + pub fn test_add(env: Env, num: u32) -> bool { let sum = Self::add(env, num, 5); sum == num as u64 + 5 } + + + pub fn test_add_i64_comm(env: Env, first: i64, second: i64) -> bool { + let a = Self::add_i64(env.clone(), first, second); + let b = Self::add_i64(env, second, first); + + a == b + } + + pub fn test_increment_i128(env: Env, x: i128) -> bool { + x == i128::MAX || x == Self::increment_i128(env, x) - 1 + } + } mod test; diff --git a/src/tests/integration/data/soroban/contracts/test_integers/Cargo.toml b/src/tests/integration/data/soroban/contracts/test_integers/Cargo.toml new file mode 100644 index 00000000..fdee533e --- /dev/null +++ b/src/tests/integration/data/soroban/contracts/test_integers/Cargo.toml @@ -0,0 +1,15 @@ +[package] +name = "test_integers" +version = "0.0.0" +edition = "2021" +publish = false + +[lib] +crate-type = ["cdylib"] +doctest = false + +[dependencies] +soroban-sdk = { workspace = true } + +[dev-dependencies] +soroban-sdk = { workspace = true, features = ["testutils"] } diff --git a/src/tests/integration/data/soroban/contracts/test_integers/README.md b/src/tests/integration/data/soroban/contracts/test_integers/README.md new file mode 100644 index 00000000..10424c19 --- /dev/null +++ b/src/tests/integration/data/soroban/contracts/test_integers/README.md @@ -0,0 +1,18 @@ +A quick example of a contract that can be ran with `komet test` + +You will need to have the stellar cli utils installed: +https://developers.stellar.org/docs/build/smart-contracts/getting-started/setup + +And the soroban semantics kompiled: +``` +kdist build soroban-semantics.llvm +``` + +And then (from this directory): + +```sh +soroban contract build --out-dir output +komet test output/test_integers.wasm +``` + +`komet test` should exit successfully diff --git a/src/tests/integration/data/soroban/contracts/test_integers/src/lib.rs b/src/tests/integration/data/soroban/contracts/test_integers/src/lib.rs new file mode 100644 index 00000000..7359423a --- /dev/null +++ b/src/tests/integration/data/soroban/contracts/test_integers/src/lib.rs @@ -0,0 +1,53 @@ +#![no_std] +use soroban_sdk::{contract, contractimpl, xdr::{int128_helpers::{i128_from_pieces, i128_hi, i128_lo}, FromXdr, ScVal}, Env, Val}; + +#[contract] +pub struct TestIntegersContract; + +#[contractimpl] +impl TestIntegersContract { + + pub fn i128_hi(_env: Env, x: i128) -> i64 { + i128_hi(x) + } + + pub fn i128_lo(_env: Env, x: i128) -> u64 { + i128_lo(x) + } + + pub fn i128_from_pieces(_env: Env, hi: i64, lo: u64) -> i128 { + i128_from_pieces(hi, lo) + } + + ///////////////////////////////////////////////////////////////////// + /// Properties + /// + + pub fn test_i128_roundtrip(env: Env, x: i128) -> bool { + let hi = Self::i128_hi(env.clone(), x); + let lo = Self::i128_lo(env.clone(), x); + let y = Self::i128_from_pieces(env, hi, lo); + + x == y + } + + pub fn test_i128_roundtrip_2(env: Env, hi: i64, lo: u64) -> bool { + let x = Self::i128_from_pieces(env.clone(), hi, lo); + let hi2 = Self::i128_hi(env.clone(), x); + let lo2 = Self::i128_lo(env, x); + + hi == hi2 && lo == lo2 + } + + // hi < 0 iff x < 0 + pub fn test_i128_hi_negativity(env: Env, x: i128) -> bool { + let hi = Self::i128_hi(env, x); + (x < 0) == (hi < 0) + } + + // hi < 0 iff x < 0 + pub fn test_i128_hi_negativity_2(env: Env, hi: i64, lo: u64) -> bool { + let x = Self::i128_from_pieces(env, hi, lo); + (x < 0) == (hi < 0) + } +} diff --git a/src/tests/integration/test_integration.py b/src/tests/integration/test_integration.py index 35826f55..e0ac2233 100644 --- a/src/tests/integration/test_integration.py +++ b/src/tests/integration/test_integration.py @@ -51,7 +51,7 @@ def test_prove_adder(tmp_path: Path, symbolic_kasmer: Kasmer) -> None: contract_wasm = symbolic_kasmer.build_soroban_contract(SOROBAN_CONTRACTS_DIR / 'test_adder', tmp_path) # Then - symbolic_kasmer.deploy_and_prove(contract_wasm, (), tmp_path) + symbolic_kasmer.deploy_and_prove(contract_wasm, (), 'test_add', tmp_path) def test_bindings(tmp_path: Path, concrete_kasmer: Kasmer) -> None: