add comments

runtimeverification · Jul 29, 2024 · b922ced · b922ced
1 parent e8cb79c
commit b922ced
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 1 deletion.
diff --git 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
                  ...
         </instrs>
         <locals>
-          0 |-> < i64 > NEW_SEQ_NUM
+          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

diff --git a/src/ksoroban/kdist/soroban-semantics/configuration.md b/src/ksoroban/kdist/soroban-semantics/configuration.md
@@ -42,6 +42,13 @@ 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>