refactor: version-based ThreadTimestamps (#2099)

[OlivierBBB]

Closes #2099.

What

Replaces the base+offset stamp lattice with SSA-style integer versioning, as proposed in #2099: within one row, the k-th movement (memory access or effectful call) executed on a path advances the stamp from version k-1 to version k, and each version names one register.

The one rule added to the issue's sketch: the largest version live at any exit of a row binds to the canonical register (M$stamp_out, or main's computed stamp). This is what preserves the guarantee that a one-line function costs exactly one added instruction — the advance past its single access is the exit's largest version, so it writes M$stamp_out directly. Advances whose result is never observed (e.g. past the last access before a fail) are retracted.

What this deletes

• the 7 stampValue kinds with position-tagged bases (callOut@pc, norm@pc, merge@pc) and their two-phase resolution through the temps map (resolve() and its "unresolved stamp temporary" panic);
• branch normalisation (stampNorm): a version is a register on every path, so branches need no parking temp;
• the forced merge of agreeing states at landings: paths arriving with the same version need no equalising copies (the old scheme inserted one per path whenever the agreed value had a non-zero offset).

The dataflow value is now {version, lit, canon} with join = max; auditing "the k-th access executed carries stamp_in + k" is a local check against the version at each access.

Cost (linea riscv corpus, zkc compile --bci, all 102 functions)

metric	before	after
instructions	8087	7913 (−174)
row structure	—	byte-identical
one-line functions	1 added instruction	1 added instruction

Wins come from dropped merge copies and from calls returning their updated stamp directly into M$stamp_out (e.g. interpreter −20, permutation −18, main −36). Four functions pay +12 total (write_16 +2, read_32 +2, full_round +4, read_and_pad_64 +4): when two sibling branches each perform an access, both define the same version register, and the path that exits early keeps a definition only the other path consumes. Recovering those 12 requires either per-path register identities (the position tags this PR removes) or value-chain folding with reachability-based retraction — both were implemented and measured, and cost more complexity than this refactor saves, so the +12 is accepted deliberately.

Testing

• full ZkC suite (Test_ZkcUnit|Test_ZkcMixed|Test_ZkcInvalid), race detector, lint: green;
• rows verified identical on the full riscv corpus, so vectorisation interplay is unchanged.

🤖 Generated with Claude Code

[Copilot]

Pull request overview

Refactors the ZkC VM timestamp-threading transform to use SSA-style integer “versions” instead of the prior base+offset stamp lattice, simplifying merge handling and removing the need for position-tagged temporaries and resolution.

Changes:

• Replaces symbolic stamp “location” tracking with per-effect versioning (join = max), and performs merge equalisation by copying into the merged version’s register.
• Reworks the rewrite sweep to bind (effect, version) → register per row, advance versions on movements, and retract unused post-access “bumps”.
• Simplifies branch handling by removing prior branch-point normalisation, retaining only the jump-table canonicalisation special case.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated no comments.

File	Description
pkg/zkc/vm/internal/transform/thread_timestamps.go	Updates the rewrite sweep to SSA-style version→register binding, merge equalisation via copies, and bump retraction for unobserved advances.
pkg/zkc/vm/internal/transform/stamp_analysis.go	Replaces the symbolic base+offset lattice with a forward DFA computing per-effect stamp versions (with join=max) and exit canonicalisation rules.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.