diff --git a/package/version b/package/version index e8e277f..04c5555 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.16 +0.1.17 diff --git a/pyproject.toml b/pyproject.toml index c182fe8..3f59898 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "ksoroban" -version = "0.1.16" +version = "0.1.17" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", diff --git a/src/ksoroban/kdist/soroban-semantics/configuration.md b/src/ksoroban/kdist/soroban-semantics/configuration.md index 9bb0611..cac07a7 100644 --- a/src/ksoroban/kdist/soroban-semantics/configuration.md +++ b/src/ksoroban/kdist/soroban-semantics/configuration.md @@ -45,6 +45,12 @@ module CONFIG ```k .Map // Map of ScVal to ScVal +``` + +- `contractLiveUntil`: The ledger sequence number until which the contract instance will live. + +```k + 0 @@ -60,7 +66,13 @@ module CONFIG ```k .Map // Map of StorageKey to ScVal - .Map + + + .Bytes + 0 + #emptyModule() + + ``` - `ledgerSequenceNumber`: The current block (or "ledger" in Stellar) number. diff --git a/src/ksoroban/kdist/soroban-semantics/host/ledger.md b/src/ksoroban/kdist/soroban-semantics/host/ledger.md index 8987300..4fafa5b 100644 --- a/src/ksoroban/kdist/soroban-semantics/host/ledger.md +++ b/src/ksoroban/kdist/soroban-semantics/host/ledger.md @@ -130,6 +130,83 @@ module HOST-LEDGER ``` +## extend_current_contract_instance_and_code_ttl + +```k + rule [hostfun-extend-current-contract-instance-and-code-ttl]: + hostCall ( "l" , "8" , [ i64 i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => loadObject(HostVal(EXTEND_TO)) + ~> loadObject(HostVal(THRESHOLD)) + ~> extendContractTtl(CONTRACT) + ~> loadObject(HostVal(EXTEND_TO)) + ~> loadObject(HostVal(THRESHOLD)) + ~> extendContractCodeTtl(CONTRACT) + ~> toSmall(Void) + ... + + + 0 |-> < i64 > THRESHOLD // U32 + 1 |-> < i64 > EXTEND_TO // U32 + + CONTRACT + + // If the TTL for the contract is less than or equal to `THRESHOLD`, + // update + syntax InternalInstr ::= extendContractTtl(ContractId) [symbol(extendContractTtl)] + // ------------------------------------------------------------------------------- + rule [extendContractTtl]: + extendContractTtl(CONTRACT) => .K ... + U32(THRESHOLD) : U32(EXTEND_TO) : S => S + + CONTRACT + 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 still alive + + syntax Int ::= extendedLiveUntil(Int, Int, Int, Int) [function, total] + // ----------------------------------------------------------------------------------- + rule extendedLiveUntil(SEQ, LIVE_UNTIL, THRESHOLD, EXTEND_TO) => SEQ +Int EXTEND_TO + requires LIVE_UNTIL -Int SEQ <=Int THRESHOLD // CURRENT_TTL <= THRESHOLD + andBool LIVE_UNTIL LIVE_UNTIL + [owise] + + syntax InternalInstr ::= extendContractCodeTtl(ContractId) [symbol(extendContractCodeTtl)] + // -------------------------------------------------------------------------------------------- + rule [extendContractCodeTtl]: + extendContractCodeTtl(CONTRACT) => extendCodeTtl(HASH) ... + + CONTRACT + HASH + ... + + + // If the TTL for the contract code is less than `THRESHOLD`, update contractLiveUntil + // where TTL is defined as LIVE_UNTIL - SEQ. + syntax InternalInstr ::= extendCodeTtl(Bytes) [symbol(extendCodeTtl)] + // ------------------------------------------------------------------------------- + rule [extendCodeTtl]: + extendCodeTtl(HASH) => .K ... + U32(THRESHOLD) : U32(EXTEND_TO) : S => S + + HASH + 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 still alive + +``` + ## Helpers ```k diff --git a/src/ksoroban/kdist/soroban-semantics/kasmer.md b/src/ksoroban/kdist/soroban-semantics/kasmer.md index 059db27..b8692e5 100644 --- a/src/ksoroban/kdist/soroban-semantics/kasmer.md +++ b/src/ksoroban/kdist/soroban-semantics/kasmer.md @@ -86,15 +86,19 @@ module KASMER [priority(55)] // ---------------------------------------------------------------------------- - rule [uploadWasm]: - uploadWasm(HASH, MOD) => .K ... - MODS => MODS [ HASH <- MOD ] - requires notBool( HASH in_keys(MODS) ) rule [uploadWasm-exists]: uploadWasm(HASH, _MOD) => .K ... - MODS - requires HASH in_keys(MODS) + HASH + + rule [uploadWasm]: + uploadWasm(HASH, MOD) => .K ... + (.Bag => + HASH + MOD + ... + ) + [priority(51)] // ----------------------------------------------------------------------------------------------------------------------- rule [deployContract-existing]: diff --git a/src/ksoroban/kdist/soroban-semantics/soroban.md b/src/ksoroban/kdist/soroban-semantics/soroban.md index 551c80f..14ddeee 100644 --- a/src/ksoroban/kdist/soroban-semantics/soroban.md +++ b/src/ksoroban/kdist/soroban-semantics/soroban.md @@ -49,7 +49,11 @@ module SOROBAN HASH ... - ... HASH |-> CODE:ModuleDecl ... + + HASH + CODE + ... + .K // rule [callContractAux-not-contract]: diff --git a/src/tests/integration/data/extend_ttl.wast b/src/tests/integration/data/extend_ttl.wast new file mode 100644 index 0000000..1cf0756 --- /dev/null +++ b/src/tests/integration/data/extend_ttl.wast @@ -0,0 +1,77 @@ + +setExitCode(1) + +uploadWasm( b"test-wasm", +;; #![no_std] +;; use soroban_sdk::{contract, contractimpl, Env}; +;; +;; #[contract] +;; pub struct IncrementContract; +;; +;; #[contractimpl] +;; impl IncrementContract { +;; pub fn extend_ttl(env: Env, threshold: u32, extend_to: u32) { +;; env.storage().instance().extend_ttl(threshold, extend_to); +;; } +;; } +(module $soroban_increment_contract.wasm + (type (;0;) (func (param i64 i64) (result i64))) + (type (;1;) (func)) + (import "l" "8" (func $_ZN17soroban_env_guest5guest6ledger45extend_current_contract_instance_and_code_ttl17h6e6604048593c195E (type 0))) + (func $extend_ttl (type 0) (param i64 i64) (result i64) + block ;; label = @1 + local.get 0 + i64.const 255 + i64.and + i64.const 4 + i64.ne + br_if 0 (;@1;) + local.get 1 + i64.const 255 + i64.and + i64.const 4 + i64.ne + br_if 0 (;@1;) + local.get 0 + i64.const -4294967292 + i64.and + local.get 1 + i64.const -4294967292 + i64.and + call $_ZN17soroban_env_guest5guest6ledger45extend_current_contract_instance_and_code_ttl17h6e6604048593c195E + drop + i64.const 2 + return + end + unreachable + unreachable) + (func $_ (type 1)) + (memory (;0;) 16) + (global $__stack_pointer (mut i32) (i32.const 1048576)) + (global (;1;) i32 (i32.const 1048576)) + (global (;2;) i32 (i32.const 1048576)) + (export "memory" (memory 0)) + (export "extend_ttl" (func $extend_ttl)) + (export "_" (func $_)) + (export "__data_end" (global 1)) + (export "__heap_base" (global 2))) +) + +setAccount(Account(b"test-account"), 9876543210) + +deployContract( + Account(b"test-account"), + Contract(b"test-sc"), + b"test-wasm", + .List +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "extend_ttl", + ListItem(U32(100)) ListItem(U32(100)), + Void +) + +setExitCode(0) \ No newline at end of file diff --git a/src/tests/integration/data/soroban/contracts/test_ttl/Cargo.toml b/src/tests/integration/data/soroban/contracts/test_ttl/Cargo.toml new file mode 100644 index 0000000..3b30c2d --- /dev/null +++ b/src/tests/integration/data/soroban/contracts/test_ttl/Cargo.toml @@ -0,0 +1,15 @@ +[package] +name = "test_ttl" +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_ttl/README.md b/src/tests/integration/data/soroban/contracts/test_ttl/README.md new file mode 100644 index 0000000..1ee6586 --- /dev/null +++ b/src/tests/integration/data/soroban/contracts/test_ttl/README.md @@ -0,0 +1,18 @@ +A quick example of a contract that can be ran with `ksoroban 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 +ksoroban test output/test_adder.wasm +``` + +`ksoroban test` should exit successfully 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 new file mode 100644 index 0000000..df57765 --- /dev/null +++ b/src/tests/integration/data/soroban/contracts/test_ttl/src/lib.rs @@ -0,0 +1,44 @@ +#![no_std] +use soroban_sdk::{contract, contractimpl, Env, Val}; + +#[contract] +pub struct TtlContract; + +extern "C" { + fn kasmer_set_ledger_sequence(x : u64); +} + +fn set_ledger_sequence(x: u32) { + unsafe { + kasmer_set_ledger_sequence(Val::from_u32(x).to_val().get_payload()); + } +} + +#[contractimpl] +impl TtlContract { + + pub fn test_ttl( + env: Env, + init_live_until: 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); + + // When: + env.storage().instance().extend_ttl(threshold, extend_to); + } + + // Since there is no getter function for the TTL value, we cannot verify + // if `extend_ttl` works as expected. + // Currently, we only check if the function runs without errors. + // Consider adding a custom hook to retrieve the TTL value for more thorough testing. + true + } +}