Fragmentation in `SparseBytes` caused by `replaceAtZ` rule

Background

SparseBytes is the data structure used for memory representation. Instead of storing a full byte array, memory is kept as a list of chunks: empty regions (#empty(N)) and concrete byte blocks (#bytes(Bs)). The memory always starts as a single #empty(N) chunk, where N is the size of the initial memory. When writes occur, empty regions are split and #bytes chunks are inserted in their place. This structure keeps large mostly-empty memories efficient, but relies on chunks remaining as coarse-grained as possible.

SparseBytes was introduced as an optimization for the MultiverseX semantics and Kasmer, where contracts often had very large memories with huge untouched regions. This representation significantly reduced configuration size and made symbolic execution feasible on those workloads.

Description

The following replaceAtZ rule in the SparseBytes implementation introduces unnecessary fragmentation.

https://github.com/runtimeverification/wasm-semantics/blob/91637f94f0f0944716ba3989ecce2a620df4fb79/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm-data/sparse-bytes.k#L165-L169

When writing to the end of an #empty chunk, the rule always creates a new #bytes chunk, even if the next chunk in REST is already a #bytes chunk. This leads to an explosion of adjacent small chunks under workloads with many small writes (e.g., copying an array from host to memory). This rule blindly inserts a new SBChunk(#bytes(Bs)) in front of REST. If REST begins with another #bytes chunk, the two byte blocks should logically be adjacent, but the rule keeps them separate. Over time this produces significant fragmentation in the SparseBytes list.

Proposed fix

Before creating a new chunk, check whether REST begins with a #bytes chunk. If it does, merge Bs with that chunk instead of prepending a new one. This keeps consecutive byte regions contiguous and prevents unnecessary list growth.

Start by reading pykwasm/kdist/wasm-semantics/wasm-data/sparse-bytes.k around the replaceAtZ rule at lines 165-169, along with the surrounding SparseBytes rules. Trace how REST is handled when it begins with #bytes, then verify that adjacent byte regions are merged and that writes no longer create unnecessary chunks.