diff --git a/src/ksoroban/kdist/soroban-semantics/cheatcodes.md b/src/ksoroban/kdist/soroban-semantics/cheatcodes.md
index 6efcea8..9e80ee1 100644
--- a/src/ksoroban/kdist/soroban-semantics/cheatcodes.md
+++ b/src/ksoroban/kdist/soroban-semantics/cheatcodes.md
@@ -7,6 +7,8 @@ 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);
// }
@@ -16,7 +18,7 @@ module CHEATCODES
...
- 0 |-> < i64 > NEW_SEQ_NUM
+ 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
diff --git a/src/ksoroban/kdist/soroban-semantics/configuration.md b/src/ksoroban/kdist/soroban-semantics/configuration.md
index 42b511a..be4d9e6 100644
--- a/src/ksoroban/kdist/soroban-semantics/configuration.md
+++ b/src/ksoroban/kdist/soroban-semantics/configuration.md
@@ -42,6 +42,13 @@ 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/tests/integration/data/ledger_sequence_get_set.wast b/src/tests/integration/data/ledger_sequence_get_set.wast
index 6a42d52..0e6989d 100644
--- a/src/tests/integration/data/ledger_sequence_get_set.wast
+++ b/src/tests/integration/data/ledger_sequence_get_set.wast
@@ -8,8 +8,12 @@ uploadWasm( b"test-wasm",
;; #[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" {
-;; // (import "env" "kasmer_set_ledger_sequence" (func $kasmer_set_ledger_sequence (param i64)))
;; fn kasmer_set_ledger_sequence(x : u64);
;; }