diff --git a/package/version b/package/version index 9f42295..5786113 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.37 +0.1.38 diff --git a/pyproject.toml b/pyproject.toml index 7ae2b8a..e44b682 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "komet" -version = "0.1.37" +version = "0.1.38" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", diff --git a/src/komet/kdist/soroban-semantics/cheatcodes.md b/src/komet/kdist/soroban-semantics/cheatcodes.md index 7a23d1d..fa1233a 100644 --- a/src/komet/kdist/soroban-semantics/cheatcodes.md +++ b/src/komet/kdist/soroban-semantics/cheatcodes.md @@ -34,6 +34,37 @@ module CHEATCODES requires getTag(HostVal(NEW_SEQ_NUM)) ==Int getTag(U32(0)) // check `NEW_SEQ_NUM` is a U32 ``` +## kasmer_set_ledger_timestamp + +```rust + extern "C" { + fn kasmer_set_ledger_timestamp(x : u64); + } +``` + +```k + rule [kasmer-set-ledger-timestamp]: + hostCall ( "env" , "kasmer_set_ledger_timestamp" , [ i64 .ValTypes ] -> [ .ValTypes ] ) + => loadObject(HostVal(TIMESTAMP)) + ~> setLedgerTimestamp + ~> toSmall(Void) + ... + + + 0 |-> < i64 > TIMESTAMP // U64 HostVal + + requires getTag(HostVal(TIMESTAMP)) ==Int 6 // check `NEW_SEQ_NUM` is a U64 + orBool getTag(HostVal(TIMESTAMP)) ==Int 64 + + syntax InternalInstr ::= "setLedgerTimestamp" + // --------------------------------------------- + rule [setLedgerTimestamp]: + setLedgerTimestamp => .K ... + U64(TIMESTAMP) : S => S + _ => TIMESTAMP + +``` + ## kasmer_create_contract ```rust diff --git a/src/komet/kdist/soroban-semantics/configuration.md b/src/komet/kdist/soroban-semantics/configuration.md index 1c10a31..6053cba 100644 --- a/src/komet/kdist/soroban-semantics/configuration.md +++ b/src/komet/kdist/soroban-semantics/configuration.md @@ -81,6 +81,7 @@ module CONFIG ```k 0 + 0 .List diff --git a/src/komet/kdist/soroban-semantics/host/context.md b/src/komet/kdist/soroban-semantics/host/context.md index 3c146c4..2e1a3cd 100644 --- a/src/komet/kdist/soroban-semantics/host/context.md +++ b/src/komet/kdist/soroban-semantics/host/context.md @@ -61,6 +61,21 @@ Return the current ledger sequence number as `U32`. SEQ_NUM ``` +## get_ledger_timestamp + +Return the current ledger timestamp as `U64`. + +```k + rule [hostfun-get-ledger-timestamp]: + hostCall ( "x" , "4" , [ .ValTypes ] -> [ i64 .ValTypes ] ) + => allocObject(U64(TIMESTAMP)) + ~> returnHostVal + ... + + .Map + TIMESTAMP +``` + ## fail_with_error ```k diff --git a/src/komet/kdist/soroban-semantics/host/ledger.md b/src/komet/kdist/soroban-semantics/host/ledger.md index 4fafa5b..c22cca8 100644 --- a/src/komet/kdist/soroban-semantics/host/ledger.md +++ b/src/komet/kdist/soroban-semantics/host/ledger.md @@ -31,7 +31,7 @@ module HOST-LEDGER putContractData(#instance) => toSmall(Void) ... KEY : VAL : S => S CONTRACT - + CONTRACT STORAGE => STORAGE [ KEY <- VAL ] ... @@ -71,7 +71,7 @@ module HOST-LEDGER KEY : S => S CONTRACT - + CONTRACT STORAGE ... @@ -112,7 +112,7 @@ module HOST-LEDGER KEY : S => S CONTRACT - + CONTRACT ... KEY |-> VAL ... ... @@ -130,6 +130,43 @@ module HOST-LEDGER ``` +## del_contract_data + +```k + rule [hostfun-del-contract-data]: + hostCall ( "l" , "2" , [ i64 i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => loadObjectFull(HostVal(KEY)) + ~> delContractData(Int2StorageType(STORAGE_TYPE)) + ... + + + 0 |-> < i64 > KEY // HostVal + 1 |-> < i64 > STORAGE_TYPE // 0: temp, 1: persistent, 2: instance + + requires Int2StorageTypeValid(STORAGE_TYPE) + + syntax InternalInstr ::= delContractData(StorageType) [symbol(delContractData)] + // --------------------------------------------------------------------------------- + rule [delContractData-instance]: + delContractData(#instance) => toSmall(Void) ... + KEY : S => S + CONTRACT + + CONTRACT + MAP => MAP [ KEY <- undef ] + ... + + requires KEY in_keys(MAP) + + rule [delContractData-other]: + delContractData(DUR:Durability) => toSmall(Void) ... + KEY : S => S + CONTRACT + MAP => MAP [#skey(CONTRACT, DUR, KEY) <- undef ] + requires #skey(CONTRACT, DUR, KEY) in_keys(MAP) + +``` + ## extend_current_contract_instance_and_code_ttl ```k diff --git a/src/komet/kdist/soroban-semantics/host/vector.md b/src/komet/kdist/soroban-semantics/host/vector.md index 47c0c74..5e3a257 100644 --- a/src/komet/kdist/soroban-semantics/host/vector.md +++ b/src/komet/kdist/soroban-semantics/host/vector.md @@ -24,6 +24,86 @@ module HOST-VECTOR .Map ``` +## vec_get + +```k + rule [hostfun-vec-get]: + hostCall ( "v" , "1" , [ i64 i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => loadObject(HostVal(INDEX)) + ~> loadObject(HostVal(VEC)) + ~> vecGet + ... + + + 0 |-> < i64 > VEC + 1 |-> < i64 > INDEX + + + syntax InternalInstr ::= "vecGet" [symbol(vecGet)] + // ---------------------------------------------------- + rule [vecGet]: + vecGet => VEC {{ I }} orDefault HostVal(0) ... // use 'orDefault' to avoid non-total list lookup + ScVec(VEC) : U32(I) : S => S + requires 0 <=Int I + andBool I hostCall ( "v" , "3" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => loadObject(HostVal(VEC)) + ~> vecLen + ... + + + 0 |-> < i64 > VEC + + + syntax InternalInstr ::= "vecLen" [symbol(vecLen)] + // ---------------------------------------------------- + rule [vecLen]: + vecLen => toSmall(U32(size(VEC))) ... + ScVec(VEC) : S => S + +``` + +## vec_push_back + +Creates a new vector by appending a given item to the end of the provided vector. +This function does not modify the original vector, maintaining immutability. +Returns a new vector with the appended item. + +```k + rule [hostfun-vec-push-back]: + hostCall ( "v" , "6" , [ i64 i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => loadObject(HostVal(VEC)) + ~> vecPushBack(HostVal(ITEM)) + ... + + + 0 |-> < i64 > VEC + 1 |-> < i64 > ITEM + + + syntax InternalInstr ::= vecPushBack(HostVal) [symbol(vecPushBack)] + // ---------------------------------------------------- + rule [vecPushBack]: + vecPushBack(ITEM) + => allocObject( + ScVec( + VEC ListItem(rel2abs(RELS, ITEM)) + ) + ) + ~> returnHostVal + ... + + ScVec(VEC) : S => S + RELS +``` + ## vec_unpack_to_linear_memory ```k diff --git a/src/tests/integration/data/soroban/contracts/test_containers/Cargo.toml b/src/tests/integration/data/soroban/contracts/test_containers/Cargo.toml new file mode 100644 index 0000000..24d1c9f --- /dev/null +++ b/src/tests/integration/data/soroban/contracts/test_containers/Cargo.toml @@ -0,0 +1,15 @@ +[package] +name = "test_containers" +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_containers/src/lib.rs b/src/tests/integration/data/soroban/contracts/test_containers/src/lib.rs new file mode 100644 index 0000000..4d1e6ab --- /dev/null +++ b/src/tests/integration/data/soroban/contracts/test_containers/src/lib.rs @@ -0,0 +1,29 @@ +#![no_std] +use soroban_sdk::{contract, contractimpl, Env, Vec}; + +#[contract] +pub struct ContainersContract; + +#[contractimpl] +impl ContainersContract { + + pub fn test_vector(env: Env, n: u32) -> bool { + let n = n % 100; + + let mut vec: Vec = Vec::new(&env); + assert_eq!(vec.len(), 0); + + for i in 0..n { + vec.push_back(i); + } + + assert_eq!(vec.len(), n); + + for i in 0..n { + assert_eq!(vec.get_unchecked(i), i); + } + + true + } + +} diff --git a/src/tests/integration/data/soroban/contracts/test_storage/src/lib.rs b/src/tests/integration/data/soroban/contracts/test_storage/src/lib.rs index ec1ce00..892861f 100644 --- a/src/tests/integration/data/soroban/contracts/test_storage/src/lib.rs +++ b/src/tests/integration/data/soroban/contracts/test_storage/src/lib.rs @@ -23,11 +23,37 @@ impl StorageContract { } pub fn test_u32_overwrite(env: Env, num1: u32, num2: u32) -> bool { - env.storage().instance().set(&INST_KEY, &num1); - env.storage().instance().set(&INST_KEY, &num2); - - let num: u32 = env.storage().instance().get(&INST_KEY).unwrap(); - - num == num2 - } + env.storage().instance().set(&INST_KEY, &num1); + env.storage().instance().set(&INST_KEY, &num2); + + let num: u32 = env.storage().instance().get(&INST_KEY).unwrap(); + + num == num2 + } + + pub fn test_set_remove_u64(env: Env, x: u64) -> bool { + // instance storage + env.storage().instance().set(&INST_KEY, &x); + assert!(env.storage().instance().has(&INST_KEY)); + + env.storage().instance().remove(&INST_KEY); + assert!(!env.storage().instance().has(&INST_KEY)); + + // temporary storage + env.storage().temporary().set(&TEMP_KEY, &x); + assert!(env.storage().temporary().has(&TEMP_KEY)); + + env.storage().temporary().remove(&TEMP_KEY); + assert!(!env.storage().temporary().has(&TEMP_KEY)); + + + // persistent storage + env.storage().persistent().set(&PRST_KEY, &x); + assert!(env.storage().persistent().has(&PRST_KEY)); + + env.storage().persistent().remove(&PRST_KEY); + assert!(!env.storage().persistent().has(&PRST_KEY)); + + true + } } 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 df57765..53a99dd 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 @@ -1,11 +1,15 @@ #![no_std] -use soroban_sdk::{contract, contractimpl, Env, Val}; +use soroban_sdk::{contract, contractimpl, Env, FromVal, Val}; #[contract] pub struct TtlContract; extern "C" { + fn kasmer_set_ledger_sequence(x : u64); + + fn kasmer_set_ledger_timestamp(x : u64); + } fn set_ledger_sequence(x: u32) { @@ -14,6 +18,12 @@ fn set_ledger_sequence(x: u32) { } } +fn set_ledger_timestamp(env: &Env, x: u64) { + unsafe { + kasmer_set_ledger_timestamp(Val::from_val(env, &x).get_payload()); + } +} + #[contractimpl] impl TtlContract { @@ -41,4 +51,10 @@ impl TtlContract { // Consider adding a custom hook to retrieve the TTL value for more thorough testing. true } + + pub fn test_timestamp(env: Env, t: u64) -> bool { + set_ledger_timestamp(&env, t); + env.ledger().timestamp() == t + } + } diff --git a/src/tests/integration/data/timestamp.wast b/src/tests/integration/data/timestamp.wast new file mode 100644 index 0000000..f4a62d4 --- /dev/null +++ b/src/tests/integration/data/timestamp.wast @@ -0,0 +1,173 @@ + +setExitCode(1) +;; #![no_std] +;; use soroban_sdk::{contract, contractimpl, Env, FromVal, Val}; +;; +;; #[contract] +;; pub struct TtlContract; +;; +;; extern "C" { +;; fn kasmer_set_ledger_timestamp(x : u64); +;; } +;; +;; fn set_ledger_timestamp(env: &Env, x: u64) { +;; unsafe { +;; kasmer_set_ledger_timestamp(Val::from_val(env, &x).get_payload()); +;; } +;; } +;; +;; #[contractimpl] +;; impl TtlContract { +;; pub fn test_timestamp(env: Env, t: u64) -> bool { +;; set_ledger_timestamp(&env, t); +;; env.ledger().timestamp() == t as u64 +;; } +;; } +uploadWasm( b"test-wasm", +(module + (type (;0;) (func (param i64) (result i64))) + (type (;1;) (func (param i64))) + (type (;2;) (func (result i64))) + (type (;3;) (func (param i32))) + (type (;4;) (func)) + (import "i" "0" (func (;0;) (type 0))) + (import "i" "_" (func (;1;) (type 0))) + (import "env" "kasmer_set_ledger_timestamp" (func (;2;) (type 1))) + (import "x" "4" (func (;3;) (type 2))) + (func (;4;) (type 0) (param i64) (result i64) + (local i32 i32 i64) + global.get 0 + i32.const 16 + i32.sub + local.tee 1 + global.set 0 + block ;; label = @1 + block ;; label = @2 + block ;; label = @3 + block ;; label = @4 + local.get 0 + i32.wrap_i64 + i32.const 255 + i32.and + local.tee 2 + i32.const 64 + i32.eq + br_if 0 (;@4;) + block ;; label = @5 + local.get 2 + i32.const 6 + i32.ne + br_if 0 (;@5;) + local.get 0 + i64.const 8 + i64.shr_u + local.set 0 + br 2 (;@3;) + end + unreachable + unreachable + end + local.get 0 + call 0 + local.tee 0 + i64.const 72057594037927935 + i64.gt_u + br_if 1 (;@2;) + end + local.get 0 + i64.const 8 + i64.shl + i64.const 6 + i64.or + local.set 3 + br 1 (;@1;) + end + local.get 0 + call 1 + local.set 3 + end + local.get 3 + call 2 + block ;; label = @1 + block ;; label = @2 + call 3 + local.tee 3 + i32.wrap_i64 + i32.const 255 + i32.and + local.tee 2 + i32.const 64 + i32.eq + br_if 0 (;@2;) + block ;; label = @3 + local.get 2 + i32.const 6 + i32.ne + br_if 0 (;@3;) + local.get 3 + i64.const 8 + i64.shr_u + local.set 3 + br 2 (;@1;) + end + local.get 1 + i32.const 8 + i32.add + call 5 + unreachable + end + local.get 3 + call 0 + local.set 3 + end + local.get 1 + i32.const 16 + i32.add + global.set 0 + local.get 3 + local.get 0 + i64.eq + i64.extend_i32_u) + (func (;5;) (type 3) (param i32) + call 6 + unreachable) + (func (;6;) (type 4) + unreachable + unreachable) + (func (;7;) (type 4)) + (memory (;0;) 16) + (global (;0;) (mut i32) (i32.const 1048576)) + (global (;1;) i32 (i32.const 1048576)) + (global (;2;) i32 (i32.const 1048576)) + (export "memory" (memory 0)) + (export "test_timestamp" (func 4)) + (export "_" (func 7)) + (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" +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "test_timestamp", + ListItem(U64(123)), + SCBool(true) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "test_timestamp", + ListItem(U64(90000000000000000)), + SCBool(true) +) + +setExitCode(0) \ No newline at end of file diff --git a/src/tests/integration/data/vec.wast b/src/tests/integration/data/vec.wast index a243c31..530f7d6 100644 --- a/src/tests/integration/data/vec.wast +++ b/src/tests/integration/data/vec.wast @@ -4,9 +4,34 @@ setExitCode(1) uploadWasm( b"test-wasm", (module (import "v" "_" (func $vec_new (result i64))) + (import "v" "3" (func $vec_len (param i64) (result i64))) + (import "v" "1" (func $vec_get (param i64 i64) (result i64))) + (import "v" "6" (func $vec_push_back (param i64 i64) (result i64))) (func $create_vec (result i64) call $vec_new) - (export "create_vec" (func $create_vec))) + (func $get_len (param i64) (result i64) + local.get 0 + call $vec_len) + (func $get_item (param i64 i64) (result i64) + local.get 0 + local.get 1 + call $vec_get) + (func $push_back (param i64 i64) (result i64) + local.get 0 + local.get 1 + call $vec_push_back) + (func $push_back_immutable (param i64 i64) (result i64) + ;; push back and return the original vector + local.get 0 + local.get 1 + call $vec_push_back + drop + local.get 0) + (export "create_vec" (func $create_vec)) + (export "get_len" (func $get_len)) + (export "get_item" (func $get_item)) + (export "push_back" (func $push_back)) + (export "push_back_immutable" (func $push_back_immutable))) ) setAccount(Account(b"test-account"), 9876543210) @@ -25,4 +50,98 @@ callTx( ScVec(.List) ) +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "get_len", + ListItem( + ScVec( + ListItem(U32(1)) + ListItem(U32(2)) + ListItem(U32(3)) + ListItem(U32(4)) + ListItem(U32(5)) + ) + ), + U32(5) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "get_len", + ListItem( + ScVec( + .List + ) + ), + U32(0) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "get_item", + ListItem( + ScVec( + ListItem(U32(1)) + ListItem(U32(2)) + ListItem(U32(3)) + ListItem(U32(4)) + ListItem(U32(5)) + ) + ) + ListItem(U32(3)), + U32(4) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "push_back", + ListItem( + ScVec( + ListItem(U32(1)) + ListItem(U32(2)) + ListItem(U32(3)) + ) + ) + ListItem(U32(4)), + ScVec( + ListItem(U32(1)) + ListItem(U32(2)) + ListItem(U32(3)) + ListItem(U32(4)) + ) +) + + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "push_back", + ListItem(ScVec(.List)) + ListItem(U32(1)), + ScVec(ListItem(U32(1))) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "push_back_immutable", + ListItem( + ScVec( + ListItem(U32(1)) + ListItem(U32(2)) + ListItem(U32(3)) + ) + ) + ListItem(U32(4)), + ScVec( + ListItem(U32(1)) + ListItem(U32(2)) + ListItem(U32(3)) + ) +) + setExitCode(0) \ No newline at end of file