Implement get_ledger_sequence (#16)

* implement `get_ledger_sequence`

* implement `kasmer_set_ledger_sequence` cheatcode

* add get/set ledger sequence test

* add comments

* Set Version: 0.1.12

---------

Co-authored-by: devops <[email protected]>

package/version

@@ -1 +1 @@
-0.1.11
+0.1.12

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. <[email protected]>",

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]:
+        <instrs> hostCall ( "env" , "kasmer_set_ledger_sequence" , [ i64  .ValTypes ] -> [ .ValTypes ] )
+              => toSmall(Void)
+                 ...
+        </instrs>
+        <locals>
+          0 |-> < i64 > NEW_SEQ_NUM // U32 HostVal
+        </locals>
+        <ledgerSequenceNumber> _ => getMajor(HostVal(NEW_SEQ_NUM)) </ledgerSequenceNumber>
+      requires getTag(HostVal(NEW_SEQ_NUM)) ==Int getTag(U32(0)) // check `NEW_SEQ_NUM` is a U32
+
+endmodule
+```

src/ksoroban/kdist/soroban-semantics/configuration.md

@@ -42,6 +42,14 @@ module CONFIG
           </account>
         </accounts>
         <contractCodes> .Map </contractCodes>
+```
+
+- `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
+        <ledgerSequenceNumber> 0 </ledgerSequenceNumber>
         <logging> .List </logging>
       </soroban>
 

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]:
+        <instrs> hostCall ( "x" , "3" , [ .ValTypes ] -> [ i64  .ValTypes ] )
+              => toSmall(U32(SEQ_NUM))
+                 ...
+        </instrs>
+        <locals> .Map </locals>
+        <ledgerSequenceNumber> SEQ_NUM </ledgerSequenceNumber>
+
+endmodule
+```

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

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

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)