Trace globals

docs/tracing.md

@@ -40,6 +40,21 @@ For the formal specification of how each value and type is serialized, see [`jso
 | `instr`  | array            | The instruction and its operands encoded as a JSON array. The first element is the instruction name, followed by its operands, e.g. `i64.const 255` is encoded as `["const", "i64", 255]`. |
 | `stack`  | array            | The value stack at the time of execution. Each entry is a `[type, value]` pair, e.g. `["i64", 4]`. |
 | `locals` | object           | The local variable bindings at the time of execution, keyed by index. Each value is a `[type, value]` pair. |
+| `globals`| object           | The executing module's WebAssembly globals, keyed by **module-relative index**. Each value is a `[type, value]` pair, like `locals`. See [Globals](#globals) below. |
+
+### Globals
+
+Every instruction record carries the executing module's globals. Unlike `mem` this is repeated in full on every record and is never `null`: a module has only a handful of globals, so a consumer reads them off the current record with no scan.
+
+```json
+{"pos": 605, "instr": ["local.get", 0], "stack": [], "locals": {}, "globals": {"0": ["i32", 1048560]}}
+```
+
+The keys are **module-relative** global indices — the index space DWARF's `DW_OP_WASM_location` global operand uses — not the store-level global addresses the semantics allocate. A debugger can therefore index the object directly with a DWARF global index. This is what lets it resolve Rust variables whose location, or whose frame base, reads a global instead of the shadow stack in linear memory; at `-O0` that is `__stack_pointer`, so without this field those variables read as `<optimized out>`.
+
+A global appears only once it has been allocated, which happens after its own *initializer* has been evaluated. So the records that evaluate a module's initializers report the globals declared before them and not the one being defined: the first such record carries `{}`, the second carries global 0, and so on.
+
+Because `<globals>` is a K *cell collection* — whose generated sort cannot appear in a hand-written `syntax` declaration, so no function can take it as an argument — the tracer cannot serialize it the way it serializes the locals map. Rules have no such restriction, so the values are read live, one global per rewrite step, by walking the executing module's `<globalAddrs>` and looking up each `<globalInst>`. See `tracing.md`'s *Collecting Globals*. Nothing is mirrored and no `wasm-semantics` rule is shadowed, so the reported values cannot drift from the real ones.
 
 ### Example
 

src/komet/kdist/soroban-semantics/json-utils.md

@@ -244,17 +244,17 @@ Additional elements carry the instruction's operands — types, operator names (
 
 These functions serialize the runtime state captured at each trace point.
 
-`Locals2JSON` serializes the local variable map as a JSON object, with local indices as string keys and their values serialized with `Val2JSON`.
+`ValMap2JSON` serializes an index-keyed map of wasm values as a JSON object, with the indices as string keys and the values serialized with `Val2JSON`. It serves both the `locals` and the `globals` fields of a trace record — locals are keyed by local index, globals by module-relative global index.
 
 `ValStack2JSON` serializes the value stack as a JSON array, preserving the stack order from top to bottom.
 
 ```k
-    syntax JSON  ::= Locals2JSON(Map)    [function]
-    syntax JSONs ::= Locals2JSONs(Map)   [function]
+    syntax JSON  ::= ValMap2JSON(Map)    [function]
+    syntax JSONs ::= ValMap2JSONs(Map)   [function]
  // --------------------------------------------------
-    rule Locals2JSON( M:Map ) => { Locals2JSONs(M) }
-    rule Locals2JSONs( .Map) => .JSONs
-    rule Locals2JSONs( (I:Int |-> V:Val) REST:Map ) => Int2String(I) : Val2JSON(V), Locals2JSONs( REST )
+    rule ValMap2JSON( M:Map ) => { ValMap2JSONs(M) }
+    rule ValMap2JSONs( .Map) => .JSONs
+    rule ValMap2JSONs( (I:Int |-> V:Val) REST:Map ) => Int2String(I) : Val2JSON(V), ValMap2JSONs( REST )
 
     syntax JSON  ::= ValStack2JSON(ValStack)    [function, total]
     syntax JSONs ::= ValStack2JSONs(ValStack)   [function, total]

src/komet/kdist/soroban-semantics/tracing.md

@@ -32,29 +32,60 @@ It is currently equivalent to `Instr`, but defined as a separate sort to make th
 
 ## Internal Instructions
 
-Two internal instructions drive the tracing mechanism:
+Three internal instructions drive the tracing mechanism:
 
 - `#traceInstr(I, POS)` -- performs the actual logging of instruction `I` at binary offset `POS` (`.Int` when no offset is available, e.g. for text format programs).
+- `#collectGlobals(I, POS, TODO, ACC)` -- an intermediate state of `#traceInstr`: it reads the executing module's globals one at a time (see *Collecting Globals*) before emitting the record. `TODO` is the not-yet-read part of `<globalAddrs>` (module index |-> `<gAddr>`), `ACC` the globals read so far (module index |-> `Val`).
 - `#resetAlreadyTraced` -- resets `<alreadyTraced>` to `false` after an instruction has been traced and executed, re-enabling tracing for the next instruction.
 
 ```k
     syntax InternalInstr ::= #traceInstr(Instr, OptionalInt)         [symbol("#traceInstr")]
+                          | #collectGlobals(Instr, OptionalInt, todo: Map, acc: Map)
+                                                                    [symbol("#collectGlobals")]
     syntax HelperInstr   ::= "#resetAlreadyTraced"                   [symbol(resetAlreadyTraced)]
 ```
 
 ## Tracing Rules
 
 ### Logging
 
-The `traceInstr` rule performs the actual logging. It:
+Logging takes two phases, because the globals cannot be read in a single match (see
+*Collecting Globals* below):
 
-1. Generates the trace data for instruction `I` using the current value stack and locals.
-2. Appends it as a JSON record to the trace file.
+1. `traceInstr` picks up the executing module's `<globalAddrs>` and hands off to
+   `#collectGlobals`, which reads the globals one at a time.
+2. `collectGlobals-done` generates the trace data for instruction `I` from the current
+   value stack, locals, memory and collected globals, and appends it as a JSON record to
+   the trace file.
+
+Everything but the globals is read in phase 2. That is safe because the intervening steps
+only rewrite `#collectGlobals` at the top of `<instrs>`: no wasm instruction runs in
+between, so the value stack, locals and memory are the same as when `#traceInstr` was
+reached.
 
 ```k
     rule [traceInstr]:
-        <instrs> #traceInstr(I, POS)
-              => #appendFileJSONLn(PATH, generateInstrTrace(I, POS, STACK, LOCALS, MEM, PM))
+        <instrs> #traceInstr(I, POS) => #collectGlobals(I, POS, GADDRS, .Map) ... </instrs>
+        <curModIdx> CUR </curModIdx>
+        <moduleInst>
+          <modIdx> CUR </modIdx>
+          <globalAddrs> GADDRS </globalAddrs>
+          ...
+        </moduleInst>
+
+    // Fallback for when there is no module instance to read globals from. Reports no
+    // globals rather than getting stuck, keeping `#traceInstr` total.
+    rule [traceInstr-nomodule]:
+        <instrs> #traceInstr(I, POS) => #collectGlobals(I, POS, .Map, .Map) ... </instrs>
+      [owise]
+```
+
+Once every global has been read, the record is emitted.
+
+```k
+    rule [collectGlobals-done]:
+        <instrs> #collectGlobals(I, POS, .Map, GLOBALS)
+              => #appendFileJSONLn(PATH, generateInstrTrace(I, POS, STACK, LOCALS, MEM, PM, GLOBALS))
                  ...
         </instrs>
         <ioDir> PATH </ioDir>
@@ -74,11 +105,12 @@ The `traceInstr` rule performs the actual logging. It:
         <prevMem> PM => MEM </prevMem>
 
     // Fallback for programs without a linear memory (e.g. text-format tests): still
-    // trace, with an empty memory so `mem` is always `null`. Guarantees `#traceInstr`
-    // is always consumed even when the memory-matching rule above cannot fire.
-    rule [traceInstr-nomem]:
-        <instrs> #traceInstr(I, POS)
-              => #appendFileJSONLn(PATH, generateInstrTrace(I, POS, STACK, LOCALS, .SparseBytes, .SparseBytes))
+    // trace, with an empty memory so `mem` is always `null`. Guarantees `#collectGlobals`
+    // is always consumed even when the memory-matching rule above cannot fire. Globals
+    // are still reported here — they are collected before this rule is reached.
+    rule [collectGlobals-done-nomem]:
+        <instrs> #collectGlobals(I, POS, .Map, GLOBALS)
+              => #appendFileJSONLn(PATH, generateInstrTrace(I, POS, STACK, LOCALS, .SparseBytes, .SparseBytes, GLOBALS))
                  ...
         </instrs>
         <ioDir> PATH </ioDir>
@@ -187,6 +219,53 @@ The `#resetAlreadyTraced` appended by `insert-traceInstr` after the `#block`/`#l
       [priority(20)]
 ```
 
+### Collecting Globals
+
+Trace records report the executing module's wasm globals, but `<globals>` is a K *cell
+collection*, and those cannot be serialized the way `ValMap2JSON` serializes the locals
+map: a cell collection's generated sort (`GlobalInstCellMap`) is not usable in a
+hand-written `syntax` declaration, so no function can take the collection as an argument
+(`Could not find sorts: [GlobalInstCellMap]`).
+
+Rules have no such restriction — they just cannot match a *variable number* of
+`<globalInst>` cells at once. So `#collectGlobals` reads the globals one per rewrite step,
+draining the executing module's `<globalAddrs>` (module index |-> `<gAddr>`) into a plain
+`Map` of module index |-> `Val` and looking up each `<globalInst>` as it goes. The result
+is keyed by module index — the index space DWARF's `DW_OP_WASM_location` global operand
+uses, so a debugger can index it directly — and reads live state, so no rule outside this
+section needs to know that tracing exists.
+
+The cost is one rewrite step per global per traced instruction. A module has only a handful
+of globals, and this is dwarfed by the file append each record already performs.
+
+```k
+    rule [collectGlobals-step]:
+        <instrs> #collectGlobals(I, POS, (IDX:Int |-> GADDR:Int) TODO, ACC)
+              => #collectGlobals(I, POS, TODO, ACC [ IDX <- VAL ])
+                 ...
+        </instrs>
+        <globalInst>
+          <gAddr>  GADDR </gAddr>
+          <gValue> VAL   </gValue>
+          ...
+        </globalInst>
+      [preserves-definedness]
+```
+
+An address with no `<globalInst>` is skipped rather than reported as `null`, which a
+consumer would read as a value. `allocglobal` adds the address to `<globalAddrs>` and the
+`<globalInst>` to `<globals>` in a single step, so this rule should be unreachable; it
+exists so that a dangling address cannot wedge the tracer.
+
+```k
+    rule [collectGlobals-skip]:
+        <instrs> #collectGlobals(I, POS, (_IDX:Int |-> _GADDR:Int) TODO, ACC)
+              => #collectGlobals(I, POS, TODO, ACC)
+                 ...
+        </instrs>
+      [owise]
+```
+
 ## Instruction Filter
 
 `shouldTraceInstr` filters out instructions that should not be traced in text format programs.
@@ -399,21 +478,28 @@ Each instruction trace record is a JSON object with these fields:
   lowercase hex), or `null` when memory is unchanged. Zero-gaps are omitted; a consumer
   reconstructs memory by taking the most recent non-`null` snapshot at or before the
   record and treating unwritten bytes as `0`.
+- `globals` — the executing module's wasm globals, keyed by MODULE-RELATIVE index (a
+  decimal string, as with `locals`), each value a `[type, value]` pair. Unlike `mem` this
+  is repeated in full on every record and never `null`: a module has only a handful of
+  globals, so a consumer reads them off the current record with no scan.
 
 Records are written one per line to the trace file.
 
 ```k
-    syntax JSON ::= generateInstrTrace(Instr, OptionalInt, ValStack, Map, SparseBytes, SparseBytes)   [function]
+    syntax JSON ::= generateInstrTrace(Instr, OptionalInt, ValStack, locals: Map, SparseBytes, SparseBytes, globals: Map)   [function]
  // ---------------------------------------------------------
-    rule generateInstrTrace(I:Instr, OFFSET, VS:ValStack, LOCALS:Map, MEM:SparseBytes, PM:SparseBytes)
+    rule generateInstrTrace(I:Instr, OFFSET, VS:ValStack, LOCALS:Map, MEM:SparseBytes, PM:SparseBytes, GLOBALS:Map)
       => {
           "pos"    : #if OFFSET ==K .Int #then null #else {OFFSET}:>Int #fi ,
           "instr"  : Instr2JSON(I) ,
           "stack"  : ValStack2JSON(VS) ,
-          "locals" : Locals2JSON(LOCALS) ,
+          "locals" : ValMap2JSON(LOCALS) ,
           // Full sparse snapshot of linear memory when it changed since the previous
           // snapshot, else `null` (memory unchanged — reuse the most recent snapshot).
-          "mem"    : #if MEM ==K PM #then null #else [ memRuns(MEM, 0) ] #fi
+          "mem"    : #if MEM ==K PM #then null #else [ memRuns(MEM, 0) ] #fi ,
+          // Collected by `#collectGlobals`, already keyed by module-relative index; the
+          // same index |-> Val shape as `locals`, so the same serializer applies.
+          "globals": ValMap2JSON(GLOBALS)
       }
 
     // Serializes a SparseBytes memory as a JSON array of `{ "addr", "bytes" }` runs, one
@@ -426,14 +512,65 @@ Records are written one per line to the trace file.
     rule memRuns(SBChunk(#empty(N)) REST, OFF) => memRuns(REST, OFF +Int N)
     rule memRuns(SBChunk(#bytes(BS)) REST, OFF)
       => ({ "addr" : OFF , "bytes" : Bytes2Hex(BS) }, memRuns(REST, OFF +Int lengthBytes(BS)))
+```
+
+`generateLedgerTrace` builds the whole-transaction **ledger baseline** record: the ledger
+scalars plus every account's balance. A debugger seeds its ledger view from this and then
+replays the per-operation events (storage writes, contract calls) on top, so it can show
+chain state at any point of a recorded execution — not just the parts a contract touched.
+
+komet-node emits it once, before a transaction's steps run (see its `#traceLedger`).
+`contracts` and `codes` are reserved for the contract-instance and uploaded-code metadata
+(wasm hash, instance/code TTLs); they are emitted empty for now, and a consumer must treat
+an empty list as "not reported" rather than "none exist".
 
+```k
+    syntax JSON ::= generateLedgerTrace(sequence: Int, timestamp: Int, accounts: Map)   [function]
+ // ---------------------------------------------------------------------------------------------
+    rule generateLedgerTrace(SEQ, TS, ACCTS)
+      => {
+          "pos"       : null ,
+          "instr"     : [ "ledger" ] ,
+          "sequence"  : SEQ ,
+          "timestamp" : TS ,
+          "accounts"  : [ AccountBalances2JSONs(ACCTS) ] ,
+          "contracts" : [ .JSONs ] ,
+          "codes"     : [ .JSONs ]
+      }
+```
+
+`AccountBalances2JSONs` serializes a plain `Map` of account `Address` |-> balance. The
+`<accounts>` cell collection cannot be read here for the same reason `<globals>` cannot:
+its generated collection sort is not usable as a declared function argument in a
+hand-written module (`Could not find sorts: [AccountCellMap]`).
+
+The caller builds that `Map` by walking the `<account>` cells one per rewrite step, the
+same way `#collectGlobals` walks the globals. That walk lives in `komet-node`'s
+`#collectAccounts`, beside the `#traceLedger` step that needs it, because the ledger
+scalars it reports (`<ledgerSequenceNumber>`, `<ledgerTimestamp>`) are komet-node's cells.
+Unlike the globals there is no index to drain, so the walk instead skips accounts already
+in the accumulator.
+
+```k
+    syntax JSONs ::= AccountBalances2JSONs(Map)   [function]
+ // ----------------------------------------------------------
+    rule AccountBalances2JSONs(.Map) => .JSONs
+
+    rule AccountBalances2JSONs((ADDR:Address |-> BAL:Int) REST:Map)
+      => { "account" : Address2JSON(ADDR) , "balance" : BAL } , AccountBalances2JSONs(REST)
+
+    rule AccountBalances2JSONs((_K |-> _V) REST:Map) => AccountBalances2JSONs(REST)
+      [owise]
+```
+
+```k
     syntax JSON ::= generateHostCallTrace(String, String, Map)   [function]
  // -------------------------------------------------------------------------
     rule generateHostCallTrace(MOD, FUNC, LOCALS)
       => {
           "pos"    : null ,
           "instr"  : [ "hostCall" , MOD , FUNC ] ,
-          "locals" : Locals2JSON(LOCALS)
+          "locals" : ValMap2JSON(LOCALS)
       }
 
     syntax JSON ::= generateContractDataTrace(ContractId, StorageType, String, List)   [function]