diff --git a/package/version b/package/version index 20f4951..0e24a92 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.11 +0.1.12 diff --git a/pyproject.toml b/pyproject.toml index 558b02a..03d0aa8 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "ksoroban" -version = "0.1.11" +version = "0.1.12" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", diff --git a/src/ksoroban/kdist/soroban-semantics/cheatcodes.md b/src/ksoroban/kdist/soroban-semantics/cheatcodes.md new file mode 100644 index 0000000..9e80ee1 --- /dev/null +++ b/src/ksoroban/kdist/soroban-semantics/cheatcodes.md @@ -0,0 +1,27 @@ +# Kasmer Cheatcodes (Kasmer Host Functions) + + +```k +requires "host/hostfuns.md" + +module CHEATCODES + imports HOSTFUNS + + // TODO: Add a check to ensure these host functions are only called from a Kasmer test contract. + + // extern "C" { + // fn kasmer_set_ledger_sequence(x : u64); + // } + rule [kasmer-set-ledger-sequence]: + hostCall ( "env" , "kasmer_set_ledger_sequence" , [ i64 .ValTypes ] -> [ .ValTypes ] ) + => toSmall(Void) + ... + + + 0 |-> < i64 > NEW_SEQ_NUM // U32 HostVal + + _ => getMajor(HostVal(NEW_SEQ_NUM)) + requires getTag(HostVal(NEW_SEQ_NUM)) ==Int getTag(U32(0)) // check `NEW_SEQ_NUM` is a U32 + +endmodule +``` \ No newline at end of file diff --git a/src/ksoroban/kdist/soroban-semantics/configuration.md b/src/ksoroban/kdist/soroban-semantics/configuration.md index aba1b07..be4d9e6 100644 --- a/src/ksoroban/kdist/soroban-semantics/configuration.md +++ b/src/ksoroban/kdist/soroban-semantics/configuration.md @@ -42,6 +42,14 @@ module CONFIG .Map +``` + +- `ledgerSequenceNumber`: The current block (or "ledger" in Stellar) number. + Accessible to contracts via the `get_ledger_sequence` host function. + Set externally using `kasmer_set_ledger_sequence`. + +```k + 0 .List diff --git a/src/ksoroban/kdist/soroban-semantics/host/context.md b/src/ksoroban/kdist/soroban-semantics/host/context.md new file mode 100644 index 0000000..0337c2d --- /dev/null +++ b/src/ksoroban/kdist/soroban-semantics/host/context.md @@ -0,0 +1,24 @@ +# Context Host Functions + +```k +requires "integer.md" + +module HOST-CONTEXT + imports HOST-INTEGER +``` + +## get_ledger_sequence + +Return the current ledger sequence number as `U32`. + +```k + rule [hostfun-get-ledger-sequence]: + hostCall ( "x" , "3" , [ .ValTypes ] -> [ i64 .ValTypes ] ) + => toSmall(U32(SEQ_NUM)) + ... + + .Map + SEQ_NUM + +endmodule +``` \ No newline at end of file diff --git a/src/ksoroban/kdist/soroban-semantics/host/hostfuns.md b/src/ksoroban/kdist/soroban-semantics/host/hostfuns.md index 6697246..1f2defe 100644 --- a/src/ksoroban/kdist/soroban-semantics/host/hostfuns.md +++ b/src/ksoroban/kdist/soroban-semantics/host/hostfuns.md @@ -1,11 +1,13 @@ ```k +requires "context.md" requires "integer.md" requires "map.md" requires "symbol.md" requires "vector.md" module HOSTFUNS + imports HOST-CONTEXT imports HOST-INTEGER imports HOST-MAP imports HOST-SYMBOL diff --git a/src/ksoroban/kdist/soroban-semantics/kasmer.md b/src/ksoroban/kdist/soroban-semantics/kasmer.md index 8377e9f..059db27 100644 --- a/src/ksoroban/kdist/soroban-semantics/kasmer.md +++ b/src/ksoroban/kdist/soroban-semantics/kasmer.md @@ -1,6 +1,7 @@ ```k requires "soroban.md" +requires "cheatcodes.md" module KASMER-SYNTAX imports WASM-TEXT-SYNTAX @@ -30,6 +31,7 @@ endmodule module KASMER imports SOROBAN + imports CHEATCODES imports KASMER-SYNTAX-COMMON configuration diff --git a/src/tests/integration/data/ledger_sequence_get_set.wast b/src/tests/integration/data/ledger_sequence_get_set.wast new file mode 100644 index 0000000..0e6989d --- /dev/null +++ b/src/tests/integration/data/ledger_sequence_get_set.wast @@ -0,0 +1,97 @@ + +setExitCode(1) + +uploadWasm( b"test-wasm", +;; #![no_std] +;; use soroban_sdk::{contract, contractimpl, Env, Val}; + +;; #[contract] +;; pub struct IncrementContract; + +;; // To enable the `kasmer_set_ledger_sequence` cheatcode, we first need to declare it as an extern function +;; // The function will appear as an import from the "env" module +;; // +;; // (import "env" "kasmer_set_ledger_sequence" (func $kasmer_set_ledger_sequence (param i64))) +;; // +;; 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 IncrementContract { +;; pub fn ledger_seq(env: Env, x: u32) -> u32 { +;; set_ledger_sequence(x); +;; env.ledger().sequence() +;; } +;; } +(module $soroban_increment_contract.wasm + (type (;0;) (func (param i64))) + (type (;1;) (func (result i64))) + (type (;2;) (func (param i64) (result i64))) + (type (;3;) (func)) + (import "env" "kasmer_set_ledger_sequence" (func $kasmer_set_ledger_sequence (type 0))) + (import "x" "3" (func $_ZN17soroban_env_guest5guest7context19get_ledger_sequence17hf00ca4c800c2f287E (type 1))) + (func $ledger_seq (type 2) (param i64) (result i64) + block ;; label = @1 + local.get 0 + i64.const 255 + i64.and + i64.const 4 + i64.eq + br_if 0 (;@1;) + unreachable + unreachable + end + local.get 0 + i64.const -4294967292 + i64.and + call $kasmer_set_ledger_sequence + call $_ZN17soroban_env_guest5guest7context19get_ledger_sequence17hf00ca4c800c2f287E + i64.const -4294967296 + i64.and + i64.const 4 + i64.or) + (func $_ (type 3)) + (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 "ledger_seq" (func $ledger_seq)) + (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"), + "ledger_seq", + ListItem(U32(1)), + U32(1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "ledger_seq", + ListItem(U32(987654321)), + U32(987654321) +) + +setExitCode(0) \ No newline at end of file