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