Trace globals by RaoulSchaffranek · Pull Request #126 · runtimeverification/komet

RaoulSchaffranek · 2026-08-10T08:36:49Z

Every instruction record in the execution trace now carries a globals object: the executing module's wasm globals, keyed by module-relative index, each value a [type, value] pair like locals:

{"pos": 605, "instr": ["local.get", 0], "stack": [], "locals": {}, "globals": {"0": ["i32", 1048560]}}

Unlike mem, it's repeated in full on every record and never null. @bbyalcinkaya I'm undecided whether we should print globals in full or diff. What are your thoughts on this?

Also

Locals2JSON → ValMap2JSON, now shared by locals and globals.
generateLedgerTrace / AccountBalances2JSONs, serializers for the ledger baseline record komet-node emits before a transaction

Testing

New test_globals_tracing.py (companion to test_memory_tracing.py) traces the increment example and asserts the field is well-formed on every instruction record.

Signed-off-by: Raoul <raoul.schaffranek@runtimeverification.com>

bbyalcinkaya · 2026-08-10T11:58:20Z

+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]`).


This could potentially be implemented as a contextual function?

Big yes! I always forget contextual functions exist. Let me re-implement.

I don't think this would improve performance, but I believe implementing it would make the code much simpler and easier to follow compared to having an intermediate step.

bbyalcinkaya

Looks good to me. Approving with a few minor/optional change requests:

Summary

docs/tracing.md: It is possible to declare functions that takes configuration cell sorts as arguments. Update the paragraph that explains why #collectGlobals is implemented using rewrite rules.
#collectGlobals (optional): Consider implementing this as a contextual function if you agree that it would make the implementation simpler.
Remove the unused generateLedgerTrace.

bbyalcinkaya · 2026-08-10T12:40:05Z

+
+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.


This comment is not quite correct. It is possible to declare the generated sort name (GlobalsCell) and use it as a function argument:

syntax GlobalsCell syntax Map ::= collectGlobals(Map, GlobalsCell) [function]

That said, the function implementation following this approach may be less clear than using rewrite rules or a contextual function. I think these comments should be corrected to reflect that this is an implementation/design choice, rather than a limitation of K.

bbyalcinkaya · 2026-08-10T12:56:10Z

+  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.


I agree with this decision.

bbyalcinkaya · 2026-08-10T12:57:42Z

+```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


Dead/unused code?

Kind of. I'm working on a branch for komet-node in parallel, which actually calls generateLedgerTrace. But good catch - let me actually move this code to komet-node.

Trace records need the executing module's globals, but `<globals>` is a cell collection whose generated sort cannot appear in a `syntax` declaration, so no function could take it as an argument. The previous workaround drained `<globalAddrs>` one global per rewrite step through an intermediate `#collectGlobals` instruction, splitting logging into two phases. K's global context in function rules lifts the restriction: a function rule may match configuration cells alongside its own arguments. `moduleGlobals` and `globalVals` use it to read `<moduleInst>` and `<globalInst>` directly, so the whole record is emitted in the single step that `#traceInstr` takes. This drops `#collectGlobals` and the argument its two-phase split required -- that the value stack, locals and memory could not move while the walk ran. `moduleGlobals` takes an `OptionalInt` rather than an `Int` so that `traceInstr-nomem` can pass `<curModIdx>` through unchanged; constraining it would stop that rule's `owise` from matching when no module is current, wedging `#traceInstr` instead of tracing it. Trace output is unchanged: 1187 records against a from-scratch build of the parent commit, zero differences in content. JSON key order within `locals` and `globals` does shift, but that also moves for `locals`, which this commit does not touch -- adding and removing symbols shifts term hashes, and so the order in which `ValMap2JSONs` walks a `Map`. Both fields are documented as index-keyed objects and are read by key. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`generateLedgerTrace` and its `AccountBalances2JSONs` helper had no caller in komet. The only call site is `collectAccounts-done` in komet-node's `node.md`, which compiles komet's semantics as an include dir, so they were reachable only from downstream: untested here (komet emits no ledger record and cannot easily be made to), undocumented here (`docs/tracing.md` describes every record kind except this one), and unbuildable downstream, since komet-node pins v0.1.86, which predates them. Moving them beside their caller fixes all three. What is left behind is a pointer saying where the record is built and why komet has none. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

RaoulSchaffranek added 3 commits August 7, 2026 10:23

Tracing wasm globals

54e2d60

Refactor: don't duplicate globals in the configration

62d5ff9

Refactor: deduplicate account balances in the configuration

4b2e13e

Signed-off-by: Raoul <raoul.schaffranek@runtimeverification.com>

RaoulSchaffranek requested a review from bbyalcinkaya August 10, 2026 08:36

bbyalcinkaya reviewed Aug 10, 2026

View reviewed changes

bbyalcinkaya approved these changes Aug 10, 2026

View reviewed changes

RaoulSchaffranek and others added 2 commits August 10, 2026 14:35

RaoulSchaffranek force-pushed the feat/globals-tracing branch from 6faf6cf to 35e5a4a Compare August 11, 2026 09:51

RaoulSchaffranek and others added 4 commits August 11, 2026 09:54

Remove dead code comment

4772761

Remove incorrect code comment

8e31ce3

Merge branch 'master' into feat/globals-tracing

c94e0e4

Version bump

f09e134

RaoulSchaffranek merged commit 673087c into master Aug 11, 2026
3 of 6 checks passed

RaoulSchaffranek deleted the feat/globals-tracing branch August 11, 2026 12:48

Navigation Menu

Uh oh!

Trace globals - #126

Trace globals#126
RaoulSchaffranek merged 9 commits into
masterfrom
feat/globals-tracing

RaoulSchaffranek commented Aug 10, 2026 •

edited

Loading

Uh oh!

bbyalcinkaya Aug 10, 2026

Uh oh!

RaoulSchaffranek Aug 10, 2026

Uh oh!

bbyalcinkaya Aug 10, 2026

Uh oh!

bbyalcinkaya left a comment

Uh oh!

bbyalcinkaya Aug 10, 2026

Uh oh!

bbyalcinkaya Aug 10, 2026

Uh oh!

bbyalcinkaya Aug 10, 2026

Uh oh!

RaoulSchaffranek Aug 10, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants


		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.

Uh oh!

Conversation

RaoulSchaffranek commented Aug 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Also

Testing

Uh oh!

bbyalcinkaya Aug 10, 2026

Choose a reason for hiding this comment

Uh oh!

RaoulSchaffranek Aug 10, 2026

Choose a reason for hiding this comment

Uh oh!

bbyalcinkaya Aug 10, 2026

Choose a reason for hiding this comment

Uh oh!

bbyalcinkaya left a comment

Choose a reason for hiding this comment

Summary

Uh oh!

bbyalcinkaya Aug 10, 2026

Choose a reason for hiding this comment

Uh oh!

bbyalcinkaya Aug 10, 2026

Choose a reason for hiding this comment

Uh oh!

bbyalcinkaya Aug 10, 2026

Choose a reason for hiding this comment

Uh oh!

RaoulSchaffranek Aug 10, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

RaoulSchaffranek commented Aug 10, 2026 •

edited

Loading