Add host functions for Bytes operations (#61)

* implement `bytes_copy_from_linear_memory` * implement `bytes_new` * implement `bytes_put` * implement `bytes_get` * refactor `bytes_copy_from_linear_memory` * implement `bytes_del` * refactor hostcall implementations to use `hostCallAux` * implement `bytes_push` * implement `bytes_pop` * implement `bytes_front` `bytes_back` * implement `bytes_insert` * implement `bytes_append` * implement `bytes_slice` * allow 0 length in `bytes_insert` * add property tests * Set Version: 0.1.51 * update soroban sdk * implement `symbol_len` * Set Version: 0.1.52 --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: automergerpr-permission-manager[bot] <190534181+automergerpr-permission-manager[bot]@users.noreply.github.com>
runtimeverification · Feb 4, 2025 · 12c938f · 12c938f
1 parent 7fe5db5
commit 12c938f
Show file tree

Hide file tree

Showing 8 changed files with 739 additions and 23 deletions.
diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.51
+0.1.52
diff --git a/pyproject.toml b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "komet"
-version = "0.1.51"
+version = "0.1.52"
 description = "K tooling for the Soroban platform"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

diff --git a/src/komet/kdist/soroban-semantics/host/buffer.md b/src/komet/kdist/soroban-semantics/host/buffer.md
@@ -30,21 +30,52 @@ module HOST-BUFFER
        andBool B_POS +Int LEN <=Int lengthBytes(BYTES)
 ```
 
+## bytes_copy_from_linear_memory
+
+Reads a slice from linear memory and writes into a `Bytes` object, returning a new object.
+The `Bytes` object expands if needed, and any gap between the starting position and its current size is filled with zeros.
+
+```k
+    rule [hostCallAux-bytes-copy-from-linear-memory]:
+        <instrs> hostCallAux ( "b" , "2" )
+              => #memLoad(LM_POS, LEN)
+              ~> bytesCopyFromLinearMemory
+                  ...
+        </instrs>
+        <hostStack> ScBytes(_) : U32(B_POS) : U32(LM_POS) : U32(LEN) : _ </hostStack>
+      requires 0 <=Int B_POS
+       andBool 0 <=Int LEN
+
+    syntax InternalInstr ::= "bytesCopyFromLinearMemory"  [symbol(bytesCopyFromLinearMemory)]
+ // ------------------------------------------------------------------------------------------
+    rule [bytesCopyFromLinearMemory]:
+        <instrs> bytesCopyFromLinearMemory
+              => allocObject(
+                    ScBytes(
+                      replaceAtBytes(
+                        padRightBytes(BYTES, B_POS +Int LEN, 0),
+                        B_POS,
+                        BS
+                      )
+                    )
+                  )
+              ~> returnHostVal
+                  ...
+        </instrs>
+        <hostStack> BS:Bytes : ScBytes(BYTES) : U32(B_POS) : U32(_) : U32(LEN) : S => S </hostStack>
+
+```
+
 ## bytes_new_from_linear_memory
 
 ```k
-    rule [hostfun-bytes-new-from-linear-memory]:
-        <instrs> hostCall ( "b" , "3" , [ i64  i64  .ValTypes ] -> [ i64  .ValTypes ] )
-              => #memLoad(getMajor(HostVal(LM_POS)), getMajor(HostVal(LEN)))
+    rule [hostCallAux-bytes-new-from-linear-memory]:
+        <instrs> hostCallAux ( "b" , "3" )
+              => #memLoad(LM_POS, LEN)
               ~> bytesNewFromLinearMemory
                  ...
         </instrs>
-        <locals>
-          0 |-> < i64 > LM_POS      // U32
-          1 |-> < i64 > LEN         // U32
-        </locals>
-      requires fromSmallValid(HostVal(LM_POS))
-       andBool fromSmallValid(HostVal(LEN))
+        <hostStack> U32(LM_POS) : U32(LEN) : S => S </hostStack>
 
     syntax InternalInstr ::= "bytesNewFromLinearMemory"      [symbol(bytesNewFromLinearMemory)]
  // ---------------------------------------------------------------------------------
@@ -58,28 +89,201 @@ module HOST-BUFFER
 
 ```
 
-## bytes_len
+## bytes_new
+
+Creates an empty `Bytes` object.
 
 ```k
+    rule [hostfun-bytes-new]:
+        <instrs> hostCall ( "b" , "4" , [ .ValTypes ] -> [ i64  .ValTypes ] )
+              => allocObject(ScBytes(.Bytes))
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <locals> .Map </locals>
+```
 
-    rule [hostfun-bytes-len]:
-        <instrs> hostCall ( "b" , "8" , [ i64  .ValTypes ] -> [ i64  .ValTypes ] )
-              => loadObject(HostVal(BYTES))
-              ~> bytesLen
+## bytes_put
+
+Updates the byte at given index.
+
+```k
+    rule [hostCallAux-bytes-put]:
+        <instrs> hostCallAux ( "b" , "5" )
+              => allocObject(ScBytes( BYTES [ I <- V ] ))
+              ~> returnHostVal
                  ...
         </instrs>
-        <locals>
-          0 |-> < i64 > BYTES      // Bytes HostVal
-        </locals>
+        <hostStack> ScBytes(BYTES) : U32(I) : U32(V) : S => S </hostStack>
+      requires 0 <=Int I
+       andBool I <Int lengthBytes(BYTES)
+       andBool 0 <=Int V
+       andBool V <Int 256
+```
 
-    syntax InternalInstr ::= "bytesLen"      [symbol(bytesLen)]
- // ---------------------------------------------------------------------------------
-    rule [bytesLen]:
-        <instrs> bytesLen
+## bytes_get
+
+Gets the byte at given index.
+
+```k
+    rule [hostCallAux-bytes-get]:
+        <instrs> hostCallAux ( "b" , "6" )
+              => toSmall( U32( BYTES [I] ) )
+                 ...
+        </instrs>
+        <hostStack> ScBytes(BYTES) : U32(I) : S => S </hostStack>
+      requires 0 <=Int I
+       andBool I <Int lengthBytes(BYTES)
+```
+
+## bytes_del
+
+Updates the byte at given index.
+
+```k
+    rule [hostCallAux-bytes-del]:
+        <instrs> hostCallAux ( "b" , "7" )
+              => allocObject(
+                  ScBytes( substrBytes(BYTES, 0, I) 
+                    +Bytes substrBytes(BYTES, I +Int 1, lengthBytes(BYTES))
+                  )
+                )
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <hostStack> ScBytes(BYTES) : U32(I) : S => S </hostStack>
+      requires 0 <=Int I
+       andBool I <Int lengthBytes(BYTES)
+```
+
+## bytes_len
+
+```k
+    rule [hostCallAux-bytes-len]:
+        <instrs> hostCallAux ( "b" , "8" )
               => toSmall(U32(lengthBytes(BS)))
                  ...
         </instrs>
         <hostStack> ScBytes(BS) : S => S </hostStack>
 
+```
+
+## bytes_push
+
+Add an element to the back of the `Bytes` object
+
+```k
+    rule [hostCallAux-bytes-push]:
+        <instrs> hostCallAux ( "b" , "9" )
+              => allocObject(ScBytes( BYTES +Bytes Int2Bytes(1, V, LE) ))
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <hostStack> ScBytes(BYTES) : U32(V) : S => S </hostStack>
+      requires 0 <=Int V
+       andBool V <Int 256
+```
+
+## bytes_pop
+
+Removes the last byte of a `Bytes` object and returns the new object.
+
+```k
+    rule [hostCallAux-bytes-pop]:
+        <instrs> hostCallAux ( "b" , "a" )
+              => allocObject(ScBytes( substrBytes(BYTES, 0, lengthBytes(BYTES) -Int 1) ))
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <hostStack> ScBytes(BYTES) : S => S </hostStack>
+      requires 0 <Int lengthBytes(BYTES)
+```
+
+## bytes_front
+
+Returns the first byte of a `Bytes` object.
+
+```k
+    rule [hostCallAux-bytes-front]:
+        <instrs> hostCallAux ( "b" , "b" )
+              => toSmall(U32( BYTES[0] ))
+                 ...
+        </instrs>
+        <hostStack> ScBytes(BYTES) : S => S </hostStack>
+      requires 0 <Int lengthBytes(BYTES)
+```
+
+## bytes_back
+
+Returns the last byte of a `Bytes` object.
+
+```k
+    rule [hostCallAux-bytes-last]:
+        <instrs> hostCallAux ( "b" , "c" )
+              => toSmall(U32( BYTES[lengthBytes(BYTES) -Int 1] ))
+                 ...
+        </instrs>
+        <hostStack> ScBytes(BYTES) : S => S </hostStack>
+      requires 0 <Int lengthBytes(BYTES)
+```
+
+## bytes_insert
+
+Inserts a byte at given index. Shifts rest of the bytes to the right.
+
+```k
+    rule [hostCallAux-bytes-insert]:
+        <instrs> hostCallAux ( "b" , "d" )
+              => allocObject(
+                  ScBytes( substrBytes(BYTES, 0, I)
+                    +Bytes Int2Bytes(1, V, LE)
+                    +Bytes substrBytes(BYTES, I, lengthBytes(BYTES))
+                  )
+                )
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <hostStack> ScBytes(BYTES) : U32(I) : U32(V) : S => S </hostStack>
+      requires 0 <=Int I
+       andBool I <=Int lengthBytes(BYTES)
+       andBool 0 <=Int V
+       andBool V <Int 256
+```
+
+## bytes_append
+
+Concatenate two `Bytes` objects. Ensures that the total length fits in `u32`.
+
+```k
+    rule [hostCallAux-bytes-append]:
+        <instrs> hostCallAux ( "b" , "e" )
+              => allocObject(
+                  ScBytes( BYTES1 +Bytes BYTES2 )
+                )
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <hostStack> ScBytes(BYTES1) : ScBytes(BYTES2) : S => S </hostStack>
+      requires lengthBytes(BYTES1) +Int lengthBytes(BYTES2) <Int #pow(i32) // total length should be less than max u32
+```
+
+## bytes_slice
+
+Returns a slice of the `Bytes` object from the given start index (inclusive) to the end index (exclusive).
+
+```k
+    rule [hostCallAux-bytes-slice]:
+        <instrs> hostCallAux ( "b" , "f" )
+              => allocObject( ScBytes( substrBytes(BYTES, START, END) ) )
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <hostStack> ScBytes(BYTES) : U32(START) : U32(END) : S => S </hostStack>
+      requires 0     <=Int START
+       andBool START <=Int END
+       andBool END   <=Int lengthBytes(BYTES)
+```
+
+```k
 endmodule
 ```
diff --git a/src/komet/kdist/soroban-semantics/host/symbol.md b/src/komet/kdist/soroban-semantics/host/symbol.md
@@ -49,6 +49,17 @@ module HOST-SYMBOL
         <hostStack> (BS => Symbol(Bytes2String(BS))) : _ </hostStack>
 ```
 
+## symbol_len
+
+```k
+    rule [hostCallAux-symbol-len]:
+        <instrs> hostCallAux ( "b" , "l" )
+              => toSmall(U32(lengthString(SYM)))
+                 ...
+        </instrs>
+        <hostStack> Symbol(SYM) : S => S </hostStack>
+```
+
 ## symbol_index_in_linear_memory
 
 Linear search a `Symbol` in an array of byte slices. Return the index of the element or trap if not found.