Sparse bytes

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)

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

kwasm-lemmas.md

@@ -342,14 +342,21 @@ Arithmetic over `#getRange`:
       [simplification]
 ```
 
+`Bytes`
+
+```k
+    rule Bs  +Bytes b"" => Bs      [simplification]
+    rule b"" +Bytes Bs  => Bs      [simplification]
+```
+
 ## Functional Tests
 
 ```k
     syntax KItem ::= run ( Step ) | done ( Step )
  // ---------------------------------------------
     rule <instrs> run ( S ) => done ( S ) ... </instrs>
 
-    syntax Step ::= Bytes | Int
+    syntax Step ::= Bytes | SparseBytes | Int
  // ---------------------------
 ```
 

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