diff --git a/data.md b/data.md
index 706aec381..ed4a1b0ef 100644
--- a/data.md
+++ b/data.md
@@ -2,6 +2,8 @@ WebAssembly Data
 ================
 
 ```k
+requires "data/sparse-bytes.k"
+
 module WASM-DATA-SYNTAX
     imports WASM-DATA-COMMON-SYNTAX
 endmodule
@@ -153,7 +155,7 @@ module WASM-DATA-COMMON
     imports LIST
     imports MAP
     imports FLOAT
-    imports BYTES
+    imports SPARSE-BYTES
     imports K-EQUAL
 ```
 
@@ -580,15 +582,11 @@ Wasm memories are byte arrays, sized in pages of 65536 bytes, initialized to be
 - `#setRange(BM, START, VAL, WIDTH)` writes the integer `I` to memory as bytes (little-endian), starting at index `N`.
 
 ```k
-    syntax Bytes ::= #setBytesRange ( Bytes , Int , Bytes ) [function, total]
+    syntax SparseBytes ::= #setBytesRange ( SparseBytes , Int , Bytes ) [function, total]
  // ------------------------------------------------------------------------------
-    rule #setBytesRange(BM, START, BS) => replaceAtBytes(padRightBytes(BM, START +Int lengthBytes(BS), 0), START, BS)
-      requires          0 <=Int START
-
-    rule #setBytesRange(_, START, _ ) => .Bytes
-      requires notBool (0 <=Int START)
+    rule #setBytesRange(BM, START, BS) => replaceAt(BM, START, BS)
 
-    syntax Bytes ::= #setRange ( Bytes , Int , Int , Int ) [function, total, smtlib(setRange)]
+    syntax SparseBytes ::= #setRange ( SparseBytes , Int , Int , Int ) [function, total, smtlib(setRange)]
  // -----------------------------------------------------------------------------------------------
     rule #setRange(BM, ADDR, VAL, WIDTH) => BM
       requires notBool (0 <Int WIDTH andBool 0 <=Int VAL andBool 0 <=Int ADDR)
@@ -599,20 +597,12 @@ Wasm memories are byte arrays, sized in pages of 65536 bytes, initialized to be
 - `#getRange(BM, START, WIDTH)` reads off `WIDTH` elements from `BM` beginning at position `START`, and converts it into an unsigned integer. The function interprets the range of bytes as little-endian.
 
 ```k
-    syntax Bytes ::= #getBytesRange ( Bytes , Int , Int ) [function, total]
+    syntax Bytes ::= #getBytesRange ( SparseBytes , Int , Int ) [function, total]
  // ----------------------------------------------------------------------------
-    rule #getBytesRange(_, START, WIDTH) => .Bytes
-      requires notBool (0 <=Int START andBool 0 <=Int WIDTH)
-
-    rule #getBytesRange(BM, START, WIDTH) => substrBytes(padRightBytes(BM, START +Int WIDTH, 0), START, START +Int WIDTH)
-      requires         (0 <=Int START andBool 0 <=Int WIDTH)
-       andBool         START <Int lengthBytes(BM)
-
-    rule #getBytesRange(BM, START, WIDTH) => padRightBytes(.Bytes, WIDTH, 0)
-      requires         (0 <=Int START andBool 0 <=Int WIDTH)
-       andBool notBool (START <Int lengthBytes(BM))
+    rule #getBytesRange(BM, START, WIDTH) 
+      => padRightBytes(unwrap(substrSparseBytes(BM, START, START +Int WIDTH)), WIDTH, 0)
 
-    syntax Int ::= #getRange(Bytes, Int, Int) [function, total, smtlib(getRange)]
+    syntax Int ::= #getRange(SparseBytes, Int, Int) [function, total, smtlib(getRange)]
  // ----------------------------------------------------------------------------------
     rule #getRange( _, ADDR, WIDTH) => 0
       requires notBool (0 <Int WIDTH andBool 0 <=Int ADDR)
diff --git a/data/sparse-bytes.k b/data/sparse-bytes.k
new file mode 100644
index 000000000..4d8638be5
--- /dev/null
+++ b/data/sparse-bytes.k
@@ -0,0 +1,205 @@
+
+module SPARSE-BYTES
+  import BOOL
+  import BYTES
+  import INT
+
+  syntax SBItem ::= #empty(Int)      [symbol, klabel(SBItem:empty)]
+                  | #bytes(Bytes)    [symbol, klabel(SBItem:bytes)]
+  
+  syntax SparseBytes [hook(LIST.List)]
+  syntax SparseBytes ::= SparseBytes SparseBytes
+          [ left, function, total, hook(LIST.concat),
+            klabel(_SparseBytes_), symbol, smtlib(smt_seq_concat),
+            assoc, unit(.SparseBytes), element(SparseBytesItem),
+            format(%1%n%2)
+          ]
+  syntax SparseBytes ::= ".SparseBytes"
+          [ function, total, hook(LIST.unit), klabel(.SparseBytes),
+            symbol, smtlib(smt_seq_nil), latex(\dotCt{SparseBytes})
+          ]
+  syntax SparseBytes ::= SBChunk(SBItem)
+          [ function, total, hook(LIST.element), klabel(SparseBytesItem),
+            symbol, smtlib(smt_seq_elem)
+          ]
+
+  syntax Bytes ::= unwrap(SparseBytes)
+    [function, total, symbol, klabel(SparseBytes:unwrap)]
+// -----------------------------------------------------------------
+  rule unwrap(SBChunk(SBI) REST) => unwrap(SBI) +Bytes unwrap(REST)
+  rule unwrap(.SparseBytes)       => .Bytes
+
+  syntax SparseBytes ::= fromBytes(Bytes)
+    [function, total, symbol, klabel(SparseBytes:fromBytes)]
+// ---------------------------------------------------------
+  rule fromBytes(Bs) => SBChunk(#bytes(Bs))
+
+  syntax Bytes ::= unwrap(SBItem)
+    [function, total, symbol, klabel(SBItem:unwrap)]
+// -----------------------------------------------
+  rule unwrap(#bytes(Bs)) => Bs
+  rule unwrap(#empty(N))  => zeros(N)
+
+  syntax Bytes ::= zeros(Int) [function, total, symbol, klabel(zeros)]
+// -------------------------------------------------------------------
+  rule zeros(N) => padLeftBytes(.Bytes, size(#empty(N)), 0)
+
+  syntax Int ::= size(SparseBytes)
+    [function, total, klabel(SparseBytes:size), symbol]
+// ---------------------------------------------------
+  rule size(SBChunk(SBI)  SBS) => size(SBI) +Int size(SBS)
+  rule size(.SparseBytes)       => 0
+
+  syntax Int ::= size(SBItem)
+    [function, total, symbol, klabel(SBItem:size)]
+// -----------------------------------------------
+  rule size(#bytes(Bs)) => lengthBytes(Bs)
+  rule size(#empty(N))   => maxInt(N,0)
+
+
+  syntax SparseBytes ::= substrSparseBytes(SparseBytes, from: Int, to: Int)
+    [function, total, klabel(SparseBytes:substr), symbol]
+// ------------------------------------------------------------------------
+  rule substrSparseBytes(_, S, E) => .SparseBytes
+    requires notBool( 0 <=Int S andBool S <=Int E )
+
+  rule substrSparseBytes(.SparseBytes, S, E) => .SparseBytes
+    requires 0 <=Int S andBool S <=Int E
+
+  rule substrSparseBytes(SBChunk(SBI) REST, S, E) => substrSparseBytes(REST, S -Int size(SBI), E -Int size(SBI))
+    requires 0 <=Int S andBool S <=Int E
+     andBool size(SBI) <=Int S
+
+  rule substrSparseBytes(SBChunk(SBI) REST, S, E) 
+    => #let SUB = substrSBItem(SBI, S, E)
+       #in SUB substrSparseBytes(REST, 0, E -Int size(SBI))
+    requires 0 <=Int S andBool S <=Int E
+     andBool size(SBI) >Int S
+
+  syntax SparseBytes ::= substrSBItem(SBItem, from: Int, to: Int)
+    [function, total, klabel(SBItem:substr), symbol]
+// -------------------------------------------------------------
+  rule substrSBItem(_SBI, S, E)      => .SparseBytes
+    requires S <Int 0 orBool E <Int S
+
+  rule substrSBItem(#empty(N), S, E) => .SparseBytes
+    requires 0 <=Int S andBool S <=Int E
+     andBool N <=Int S
+
+  rule substrSBItem(#empty(N), S, E) => SBChunk( #empty( minInt(E, N) -Int S) )
+    requires 0 <=Int S andBool S <=Int E
+     andBool S <Int N
+  
+  rule substrSBItem(#bytes(Bs), S, E) => .SparseBytes
+    requires 0 <=Int S andBool S <=Int E
+     andBool          lengthBytes(Bs) <=Int S
+
+  rule substrSBItem(#bytes(Bs), S, E) 
+    => SBChunk(#bytes( substrBytes(Bs, S, minInt(E, lengthBytes(Bs))) ))
+    requires 0 <=Int S andBool S <=Int E
+     andBool S <Int lengthBytes(Bs) 
+
+
+  syntax SparseBytes ::= replaceAt(SparseBytes, Int, Bytes)
+    [function, total, symbol, klabel(SparseBytes:replaceAt)]
+// --------------------------------------------------------
+  // invalid argument
+  rule replaceAt(_, S, _) => .SparseBytes 
+    requires S <Int 0
+
+  // append
+  rule replaceAt(.SparseBytes, S, Bs) => SBChunk(#bytes(Bs))
+    requires 0 ==Int S
+
+  // append padded
+  rule replaceAt(.SparseBytes, S, Bs) => SBChunk(#empty(S)) SBChunk(#bytes(Bs))
+    requires 0 <Int S
+
+  // skip
+  rule replaceAt(SBChunk(SBI) REST, S, Bs) 
+    => SBChunk(SBI) replaceAt(REST, S -Int size(SBI), Bs)
+    requires size(SBI) <=Int S
+
+  rule replaceAt(SBChunk(#empty(N))  REST, S, Bs) => replaceAtZ(N, REST, S, Bs)
+    requires S <Int N
+  rule replaceAt(SBChunk(#bytes(B)) REST, S, Bs) => replaceAtB(B, REST, S, Bs)
+    requires S <Int lengthBytes(B)
+  
+  syntax SparseBytes ::= replaceAtZ(Int, SparseBytes, Int, Bytes)
+    [function, total, symbol, klabel(SparseBytes:replaceAtZ)]
+// ---------------------------------------------------------------
+  ////////////// S < 0
+  rule replaceAtZ(_, _, S, _) => .SparseBytes 
+    requires S <Int 0
+
+  ////////////// S > 0
+  // split zeros: 0 < S < N
+  rule replaceAtZ(N, REST, S, Bs)
+    => SBChunk(#empty(S)) replaceAtZ(N -Int S, REST, 0, Bs) 
+    requires 0 <Int S
+     andBool S <Int N
+
+  // skip zeros: 0 <= N <= S
+  rule replaceAtZ(N, REST, S, Bs)
+    => SBChunk(#empty(N)) replaceAt(REST, S -Int N, Bs) 
+    requires 0 <Int S
+     andBool 0 <=Int N
+     andBool N <=Int S
+
+  ////////////// S == 0
+  ///////// len(Bs) < N
+  rule replaceAtZ(N, REST, S, Bs)
+    => SBChunk(#bytes(Bs)) SBChunk(#empty(N -Int lengthBytes(Bs))) REST 
+    requires 0 ==Int S
+     andBool lengthBytes(Bs) <Int N
+
+  ///////// len(Bs) = N
+  rule replaceAtZ(N, REST, S, Bs)
+    => SBChunk(#bytes(Bs)) REST 
+    requires 0 ==Int S
+     andBool lengthBytes(Bs) ==Int N
+
+  ///////// len(Bs) > N
+  rule replaceAtZ(N, REST, S, Bs)
+    => replaceAt(SBChunk(#bytes(zeros(N))) REST, S, Bs) 
+    requires 0 ==Int S
+     andBool lengthBytes(Bs) >Int N
+
+
+  syntax SparseBytes ::= replaceAtB(Bytes, SparseBytes, Int, Bytes)
+    [function, total, symbol, klabel(SparseBytes:replaceAtB)]
+// ---------------------------------------------------------------
+  ////////// S + len(Bs) <= len(MB)
+  rule replaceAtB(MB, REST, S, Bs)
+    => SBChunk(#bytes( replaceAtBytes(MB, S, Bs) )) REST
+    requires 0 <=Int S
+     andBool S +Int lengthBytes(Bs) <=Int lengthBytes(MB)
+
+  ////////// S + len(Bs) > len(MB)
+  rule replaceAtB(MB, REST, S, Bs)
+    => replaceAt(
+          joinUntil(MB, REST, S +Int lengthBytes(Bs)),
+          S,
+          Bs
+        )
+    requires 0 <=Int S
+     andBool lengthBytes(MB) <Int S +Int lengthBytes(Bs) 
+
+
+  // join list items until Bs is at least I bytes
+  syntax SparseBytes ::= joinUntil(Bytes, SparseBytes, Int)
+    [function, total]
+// --------------------------------------------------------
+  rule joinUntil(Bs, REST, I)
+    => SBChunk(#bytes(Bs)) REST
+    requires I <=Int lengthBytes(Bs)
+
+  rule joinUntil(Bs,                    SBChunk(SBI) REST, I)
+    => joinUntil(Bs +Bytes unwrap(SBI), REST,              I)
+    requires I >Int lengthBytes(Bs)
+
+  rule joinUntil(Bs, .SparseBytes, I)
+    => SBChunk(#bytes( padRightBytes(Bs, I, 0) ))
+    requires I >Int lengthBytes(Bs)
+
+endmodule
diff --git a/kwasm-lemmas.md b/kwasm-lemmas.md
index 492b2ae96..f8a4c50b0 100644
--- a/kwasm-lemmas.md
+++ b/kwasm-lemmas.md
@@ -342,6 +342,13 @@ Arithmetic over `#getRange`:
       [simplification]
 ```
 
+`Bytes`
+
+```k
+    rule Bs  +Bytes b"" => Bs      [simplification]
+    rule b"" +Bytes Bs  => Bs      [simplification]
+```
+
 ## Functional Tests
 
 ```k
@@ -349,7 +356,7 @@ Arithmetic over `#getRange`:
  // ---------------------------------------------
     rule <instrs> run ( S ) => done ( S ) ... </instrs>
 
-    syntax Step ::= Bytes | Int
+    syntax Step ::= Bytes | SparseBytes | Int
  // ---------------------------
 ```
 
diff --git a/tests/proofs/functions-spec.k b/tests/proofs/functions-spec.k
index ac8dd50f6..dd6285950 100644
--- a/tests/proofs/functions-spec.k
+++ b/tests/proofs/functions-spec.k
@@ -50,4 +50,88 @@ module FUNCTIONS-SPEC
           </instrs>
        requires 0 <=Int ADDR
 
+    claim <instrs> run  ( substrSparseBytes(_SB,  S, _E) ) => done ( .SparseBytes ) ... </instrs> requires S <Int 0
+    claim <instrs> run  ( substrSparseBytes(_SB, _S,  E) ) => done ( .SparseBytes ) ... </instrs> requires E <Int 0
+    claim <instrs> run  ( substrSparseBytes(_SB,  S,  E) ) => done ( .SparseBytes ) ... </instrs> requires E <Int S
+
+    claim <instrs> run  ( #getRange(_SB,  S, _W) ) => done ( 0 ) ... </instrs> requires S <Int 0
+    claim <instrs> run  ( #getRange(_SB, _S,  W) ) => done ( 0 ) ... </instrs> requires W <Int 0
+    
+    claim <instrs> run  ( unwrap(fromBytes(Bs))) => done ( Bs ) ... </instrs>
+
+    claim <instrs> run  ( #getBytesRange(  
+                            SBChunk(#bytes(b"abcd"))
+                            SBChunk(#bytes(b"efgh")),
+                            2,
+                            4
+                          )
+                        )
+                => done ( b"cdef" )
+               ...
+          </instrs>
+
+    claim <instrs> run  ( #getBytesRange(  
+                            SBChunk(#bytes(B1))
+                            SBChunk(#empty(N1))
+                            SBChunk(#bytes(B2)),
+                            lengthBytes(B1) +Int N1,
+                            WIDTH
+                          )
+                        )
+                => done ( padRightBytes(B2, WIDTH, 0) )
+               ...
+          </instrs>
+       requires N1 ==K 123000000
+        andBool WIDTH ==K 120
+        andBool B1 ==K b"00000000000000000000000000000000asdfghjklqwertyuio"
+        andBool B2 ==K b"asdfghjklqwertyuio"
+
+    claim <instrs> run  ( #getBytesRange(  
+                            SBChunk(#bytes(B1))
+                            SBChunk(#empty(N1))
+                            SBChunk(#bytes(B2)),
+                            lengthBytes(B1) +Int N1 -Int Z,
+                            WIDTH
+                          )
+                        )
+                => done ( padRightBytes(zeros(Z) +Bytes B2, WIDTH, 0) )
+               ...
+          </instrs>
+       requires N1 ==K 123000000
+        andBool Z ==K 30
+        andBool WIDTH ==K 120
+        andBool B1 ==K b"00000000000000000000000000000000asdfghjklqwertyuio"
+        andBool B2 ==K b"asdfghjklqwertyuio"
+
+    claim <instrs> run  ( #getBytesRange(  
+                            SBChunk(#bytes(b"a"))
+                            SBChunk(#empty(1))
+                            SBChunk(#bytes(b"b"))
+                            SBChunk(#empty(1))
+                            SBChunk(#bytes(b"c"))
+                            SBChunk(#empty(1))
+                            SBChunk(#bytes(b"d"))
+                            SBChunk(#empty(1))
+                            SBChunk(#bytes(b"e")),
+                            0,
+                            100
+                          )
+                        )
+                => done ( padRightBytes(b"a\x00b\x00c\x00d\x00e", 100, 0) )
+               ...
+          </instrs>
+
+    // Should not allocate huge bytes
+    claim <instrs> run  ( #getBytesRange(  
+                            SBChunk(#empty(Z))
+                            SBChunk(#bytes(b"x")),
+                            Z -Int 1,
+                            2
+                          )
+                        )
+                => done ( b"\x00x" )
+               ...
+          </instrs>
+        requires Z ==K 1000000000000 // ~ 1 TB
+
 endmodule
diff --git a/wasm.md b/wasm.md
index f5da5e005..31d500d6a 100644
--- a/wasm.md
+++ b/wasm.md
@@ -5,6 +5,7 @@ WebAssembly State and Semantics
 require "data.md"
 require "data/list-int.k"
 require "data/map-int-to-int.k"
+require "data/sparse-bytes.k"
 require "data/tools.k"
 require "numeric.md"
 
@@ -232,10 +233,10 @@ module WASM
           <nextTabAddr> 0 </nextTabAddr>
           <mems>
             <memInst multiplicity="*" type="Map">
-              <mAddr> 0      </mAddr>
-              <mmax>  .Int   </mmax>
-              <msize> 0      </msize>
-              <mdata> .Bytes </mdata>
+              <mAddr> 0            </mAddr>
+              <mmax>  .Int         </mmax>
+              <msize> 0            </msize>
+              <mdata> .SparseBytes </mdata>
             </memInst>
           </mems>
           <nextMemAddr> 0 </nextMemAddr>
@@ -1010,7 +1011,7 @@ Sort `Signedness` is defined in module `BYTES`.
     syntax Instr ::= #load(ValType, LoadOp, offset : Int) [klabel(aLoad), symbol]
                    | "load" "{" IValType Int Int Signedness"}"
                    | "load" "{" IValType Int Int Signedness Int"}"
-                   | "load" "{" IValType Int Int Signedness Bytes"}"
+                   | "load" "{" IValType Int Int Signedness SparseBytes"}"
                    | IValType "." LoadOp Int
  // ----------------------------------------
     rule <instrs> #load(ITYPE:IValType, LOP, OFFSET) => ITYPE . LOP (IDX +Int OFFSET)  ... </instrs>
@@ -1050,8 +1051,8 @@ Sort `Signedness` is defined in module `BYTES`.
          </memInst>
       requires (EA +Int WIDTH) >Int (SIZE *Int #pageSize())
 
-    rule <instrs> load { ITYPE WIDTH EA   Signed DATA:Bytes } => #chop(< ITYPE > #signedWidth(WIDTH, #getRange(DATA, EA, WIDTH))) ... </instrs>
-    rule <instrs> load { ITYPE WIDTH EA Unsigned DATA:Bytes } => < ITYPE > #getRange(DATA, EA, WIDTH) ... </instrs>
+    rule <instrs> load { ITYPE WIDTH EA   Signed DATA:SparseBytes } => #chop(< ITYPE > #signedWidth(WIDTH, #getRange(DATA, EA, WIDTH))) ... </instrs>
+    rule <instrs> load { ITYPE WIDTH EA Unsigned DATA:SparseBytes } => < ITYPE > #getRange(DATA, EA, WIDTH) ... </instrs>
 ```
 
 The `size` operation returns the size of the memory, measured in pages.