From ebd71e1dfdaaeec50e3e45c5b08e616d81f7fee1 Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Wed, 6 Nov 2024 16:20:51 +0300 Subject: [PATCH 1/8] fix `getTag(SCBool(_))` --- src/komet/kdist/soroban-semantics/data.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 From 398b4de7bcb3b601dab3f7f9d57cbf567a0fb041 Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Wed, 6 Nov 2024 17:44:17 +0300 Subject: [PATCH 2/8] implement `update_current_contract_wasm` and add a wast test --- .../kdist/soroban-semantics/host/ledger.md | 31 ++++++++++ src/tests/integration/data/update_wasm.wast | 59 +++++++++++++++++++ 2 files changed, 90 insertions(+) create mode 100644 src/tests/integration/data/update_wasm.wast diff --git a/src/komet/kdist/soroban-semantics/host/ledger.md b/src/komet/kdist/soroban-semantics/host/ledger.md index c22cca8f..024f921c 100644 --- a/src/komet/kdist/soroban-semantics/host/ledger.md +++ b/src/komet/kdist/soroban-semantics/host/ledger.md @@ -165,6 +165,37 @@ 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_current_contract_instance_and_code_ttl 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 3a21451662c16fc203976519913ca5e431aad7e0 Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Fri, 8 Nov 2024 15:14:05 +0300 Subject: [PATCH 3/8] add live-until field to storage entries --- .../kdist/soroban-semantics/configuration.md | 4 ++- .../kdist/soroban-semantics/host/ledger.md | 35 ++++++++++++++++--- 2 files changed, 34 insertions(+), 5 deletions(-) diff --git a/src/komet/kdist/soroban-semantics/configuration.md b/src/komet/kdist/soroban-semantics/configuration.md index 6053cba0..4f51380b 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 ``` diff --git a/src/komet/kdist/soroban-semantics/host/ledger.md b/src/komet/kdist/soroban-semantics/host/ledger.md index 024f921c..6eaa6bd6 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, _) ... ``` @@ -238,7 +250,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 From 57273121b4285ff58d6ab0a218b5d71fa901dac3 Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Fri, 8 Nov 2024 15:24:11 +0300 Subject: [PATCH 4/8] implement `extend_contract_data_ttl` --- .../kdist/soroban-semantics/configuration.md | 8 ++++ .../kdist/soroban-semantics/host/ledger.md | 46 +++++++++++++++++++ 2 files changed, 54 insertions(+) diff --git a/src/komet/kdist/soroban-semantics/configuration.md b/src/komet/kdist/soroban-semantics/configuration.md index 4f51380b..ed581bb6 100644 --- a/src/komet/kdist/soroban-semantics/configuration.md +++ b/src/komet/kdist/soroban-semantics/configuration.md @@ -472,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/host/ledger.md b/src/komet/kdist/soroban-semantics/host/ledger.md index 6eaa6bd6..1e635dd0 100644 --- a/src/komet/kdist/soroban-semantics/host/ledger.md +++ b/src/komet/kdist/soroban-semantics/host/ledger.md @@ -210,6 +210,52 @@ module HOST-LEDGER ``` +## 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 ```k From 038b46e123e35e089cb8f456785304f45087174a Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Fri, 8 Nov 2024 15:24:45 +0300 Subject: [PATCH 5/8] add `storage.wast` tests --- src/tests/integration/data/storage.wast | 121 ++++++++++++++++++++++++ 1 file changed, 121 insertions(+) create mode 100644 src/tests/integration/data/storage.wast 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 From 35e6e3f43d7ca1c3358457ee0b020d98732be569 Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Mon, 11 Nov 2024 13:37:25 +0300 Subject: [PATCH 6/8] update `test_ttl` after introducing `#maxEntryTtl` --- .../soroban/contracts/test_ttl/src/lib.rs | 28 +++++++++++++------ 1 file changed, 20 insertions(+), 8 deletions(-) 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 From b4c43160d6243cf5dfe07a97c0af29e440e2f365 Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 11 Nov 2024 10:55:47 +0000 Subject: [PATCH 7/8] Set Version: 0.1.39 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 5786113b..528bd040 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.38 +0.1.39 diff --git a/pyproject.toml b/pyproject.toml index e44b6820..ef43a3d5 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "komet" -version = "0.1.38" +version = "0.1.39" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", From 38f9c166b6cfa19f256edd2f7dba8109f3acbdb5 Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 19 Nov 2024 07:29:01 +0000 Subject: [PATCH 8/8] Set Version: 0.1.41 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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. ",