Storage Host Functions (#18)

* Implement `loadObjectFull` for converting HostVals to ScVals on the stack * add wasm tests * add rust test * define storage configuration cells * implement host functions * Set Version: 0.1.14 --------- Co-authored-by: devops <[email protected]>
runtimeverification · Aug 2, 2024 · 4bb7100 · 4bb7100
1 parent 4f2496a
commit 4bb7100
Show file tree

Hide file tree

Showing 10 changed files with 902 additions and 6 deletions.
diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.13
+0.1.14
diff --git a/pyproject.toml b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "ksoroban"
-version = "0.1.13"
+version = "0.1.14"
 description = "K tooling for the Soroban platform"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/src/ksoroban/kdist/soroban-semantics/configuration.md b/src/ksoroban/kdist/soroban-semantics/configuration.md
@@ -32,7 +32,19 @@ module CONFIG
           <contract multiplicity="*" type="Map">
             <contractId> Contract(.Bytes) </contractId>
             <wasmHash> .Bytes </wasmHash>
-            <instanceStorage> .Map </instanceStorage>
+```
+
+- `instanceStorage`: Instance storage is a map from user-provided keys (ScVal) to values (ScVal), and it is tied to the
+    contract's lifecycle.
+    If the value is a container (e.g., map or vector), the contained values must also be `ScVal`, not `HostVal`.
+    Therefore, before storing data, all `HostVal`s in the data should be resolved to `ScVal`s.
+    Other storage types (persistent and temporary) are stored separately in `<contractData>`.
+
+    - [Stellar Docs](https://developers.stellar.org/docs/learn/encyclopedia/storage/persisting-data#ledger-entries)
+    - [CAP 46-05: Instance Storage](https://github.com/stellar/stellar-protocol/blob/master/core/cap-0046-05.md#instance-storage)
+
+```k
+            <instanceStorage> .Map </instanceStorage> // Map of ScVal to ScVal
           </contract>
         </contracts>
         <accounts>
@@ -41,6 +53,13 @@ module CONFIG
             <balance> 0 </balance>
           </account>
         </accounts>
+```
+- `contractData`: Stores persistent and temporary storage items separately from the contract instances.
+    The storage entries are identified by `(ContractId, Durability, ScVal)` and contain values of type `ScVal`.
+    Keys and values must be fully resolved `ScVal`s as in `<instanceStorage>`.
+
+```k
+        <contractData> .Map </contractData> // Map of StorageKey to ScVal
         <contractCodes> .Map </contractCodes>
 ```
 
@@ -59,6 +78,14 @@ module CONFIG
 
     syntax InternalCmd ::= #callResult(ValStack, List)   [symbol(#callResult)]
 
+    syntax Durability ::= "#temporary"           [symbol(#temporary)]
+                        | "#persistent"          [symbol(#persistent)]
+
+    syntax StorageType ::= Durability
+                         | "#instance"           [symbol(#instance)]
+
+    syntax StorageKey ::= #skey( ContractId , Durability , ScVal )   [symbol(StorageKey)]
+
 endmodule
 ```
 
@@ -131,25 +158,27 @@ These internal commands manages the call stack when calling and returning from a
     syntax AccountsCellFragment
     syntax ContractsCellFragment
 
-    syntax Accounts ::= "{" AccountsCellFragment "," ContractsCellFragment "}"
+    syntax Accounts ::= "{" AccountsCellFragment "," ContractsCellFragment "," Map "}"
  // --------------------------------------------------------
 
     syntax InternalCmd ::= "pushWorldState"  [symbol(pushWorldState)]
  // ---------------------------------------
     rule [pushWorldState]:
          <k> pushWorldState => .K ... </k>
-         <interimStates> (.List => ListItem({ ACCTDATA , CONTRACTS })) ... </interimStates>
+         <interimStates> (.List => ListItem({ ACCTDATA , CONTRACTS , CTRDATA })) ... </interimStates>
          <contracts> CONTRACTS </contracts>
          <accounts> ACCTDATA </accounts>
+         <contractData> CTRDATA </contractData>
       [priority(60)]
 
     syntax InternalCmd ::= "popWorldState"  [symbol(popWorldState)]
  // --------------------------------------
     rule [popWorldState]:
          <k> popWorldState => .K ... </k>
-         <interimStates> (ListItem({ ACCTDATA , CONTRACTS }) => .List) ... </interimStates>
+         <interimStates> (ListItem({ ACCTDATA , CONTRACTS , CTRDATA }) => .List) ... </interimStates>
          <contracts> _ =>  CONTRACTS </contracts>
          <accounts> _ => ACCTDATA </accounts>
+         <contractData> _ => CTRDATA </contractData>
       [priority(60)]
 
     syntax InternalCmd ::= "dropWorldState"  [symbol(dropWorldState)]
@@ -276,6 +305,7 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly
 
 ### Accessing host objects
 
+- loadObject: Load a host object from `<hostObjects>` to `<hostStack>`
 
 ```k
     syntax InternalInstr ::= loadObject(HostVal)    [symbol(loadObject)]
@@ -306,6 +336,26 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly
       requires notBool isObject(VAL)
        andBool fromSmallValid(VAL)
 
+```
+
+- loadObjectFull: Like `loadObject` but resolves all `HostVal`s in containers recursively using `HostVal2ScValRec`
+
+```k
+    syntax InternalInstr ::= loadObjectFull(HostVal)    [symbol(loadObjectFull)]
+                           | "loadObjectFullAux"
+ // --------------------------------------------------------------------
+    rule [loadObjectFull]:
+        <instrs> loadObjectFull(VAL)
+              => loadObject(VAL)
+              ~> loadObjectFullAux
+                 ...
+        </instrs>
+
+    rule [loadObjectFullAux]:
+        <instrs> loadObjectFullAux => .K ... </instrs>
+        <hostStack> (SCV => HostVal2ScValRec(SCV, OBJS, RELS)) : _ </hostStack>
+        <relativeObjects> RELS </relativeObjects>
+        <hostObjects>     OBJS </hostObjects>
 
 ```
 

diff --git a/src/ksoroban/kdist/soroban-semantics/host/hostfuns.md b/src/ksoroban/kdist/soroban-semantics/host/hostfuns.md
@@ -2,13 +2,15 @@
 ```k
 requires "context.md"
 requires "integer.md"
+requires "ledger.md"
 requires "map.md"
 requires "symbol.md"
 requires "vector.md"
 
 module HOSTFUNS
     imports HOST-CONTEXT
     imports HOST-INTEGER
+    imports HOST-LEDGER
     imports HOST-MAP
     imports HOST-SYMBOL
     imports HOST-VECTOR

diff --git a/src/ksoroban/kdist/soroban-semantics/host/ledger.md b/src/ksoroban/kdist/soroban-semantics/host/ledger.md
@@ -0,0 +1,147 @@
+# Ledger Host Functions
+
+```k
+requires "integer.md"
+
+module HOST-LEDGER
+    imports HOST-INTEGER
+
+```
+
+## put_contract_data
+
+```k
+    rule [hostfun-put-contract-data]:
+        <instrs> hostCall ( "l" , "_" , [ i64  i64  i64  .ValTypes ] -> [ i64  .ValTypes ] )
+              => loadObjectFull(HostVal(VAL))
+              ~> loadObjectFull(HostVal(KEY))
+              ~> putContractData(Int2StorageType(STORAGE_TYPE))
+                 ...
+        </instrs>
+        <locals>
+          0 |-> < i64 > KEY            // HostVal
+          1 |-> < i64 > VAL            // HostVal
+          2 |-> < i64 > STORAGE_TYPE   // 0: temp, 1: persistent, 2: instance
+        </locals>
+      requires Int2StorageTypeValid(STORAGE_TYPE)
+
+    syntax InternalInstr ::= putContractData(StorageType)   [symbol(putContractData)]
+ // ---------------------------------------------------------------------------------
+    rule [putContractData-instance]:
+        <instrs> putContractData(#instance) => toSmall(Void) ... </instrs>
+        <hostStack> KEY : VAL : S => S </hostStack>
+        <callee> CONTRACT </callee>
+        <contract> 
+          <contractId> CONTRACT </contractId>
+          <instanceStorage> STORAGE => STORAGE [ KEY <- VAL ] </instanceStorage>
+          ...
+        </contract>
+
+    rule [putContractData-other]:
+        <instrs> putContractData(DUR:Durability) => toSmall(Void) ... </instrs>
+        <hostStack> KEY : VAL : S => S </hostStack>
+        <callee> CONTRACT </callee>
+        <contractData>
+          STORAGE => STORAGE [ #skey(CONTRACT, DUR, KEY) <- VAL ]
+        </contractData>
+
+```
+
+## has_contract_data
+
+```k
+    rule [hostfun-has-contract-data]:
+        <instrs> hostCall ( "l" , "0" , [ i64  i64  .ValTypes ] -> [ i64  .ValTypes ] )
+              => loadObjectFull(HostVal(KEY))
+              ~> hasContractData(Int2StorageType(STORAGE_TYPE))
+                 ...
+        </instrs>
+        <locals>
+          0 |-> < i64 > KEY            // HostVal
+          1 |-> < i64 > STORAGE_TYPE   // 0: temp, 1: persistent, 2: instance
+        </locals>
+      requires Int2StorageTypeValid(STORAGE_TYPE)
+
+    syntax InternalInstr ::= hasContractData(StorageType)   [symbol(hasContractData)]
+ // ---------------------------------------------------------------------------------
+    rule [hasContractData-instance]:
+        <instrs> hasContractData(#instance)
+              => toSmall(SCBool( KEY in_keys(STORAGE) ))
+                 ...
+        </instrs>
+        <hostStack> KEY : S => S </hostStack>
+        <callee> CONTRACT </callee>
+        <contract> 
+          <contractId> CONTRACT </contractId>
+          <instanceStorage> STORAGE </instanceStorage>
+          ...
+        </contract>
+
+    rule [hasContractData-other]:
+        <instrs> hasContractData(DUR:Durability)
+              => toSmall(SCBool( #skey(CONTRACT, DUR, KEY) in_keys(STORAGE) ))
+                 ...
+        </instrs>
+        <hostStack> KEY : S => S </hostStack>
+        <callee> CONTRACT </callee>
+        <contractData> STORAGE </contractData>
+```
+
+## get_contract_data
+
+```k
+    rule [hostfun-get-contract-data]:
+        <instrs> hostCall ( "l" , "1" , [ i64  i64  .ValTypes ] -> [ i64  .ValTypes ] )
+              => loadObjectFull(HostVal(KEY))
+              ~> getContractData(Int2StorageType(STORAGE_TYPE))
+                 ...
+        </instrs>
+        <locals>
+          0 |-> < i64 > KEY            // HostVal
+          1 |-> < i64 > STORAGE_TYPE   // 0: temp, 1: persistent, 2: instance
+        </locals>
+      requires Int2StorageTypeValid(STORAGE_TYPE)
+
+    syntax InternalInstr ::= getContractData(StorageType)   [symbol(getContractData)]
+ // ---------------------------------------------------------------------------------
+    rule [getContractData-instance]:
+        <instrs> getContractData(#instance)
+              => allocObject(VAL)
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <hostStack> KEY : S => S </hostStack>
+        <callee> CONTRACT </callee>
+        <contract> 
+          <contractId> CONTRACT </contractId>
+          <instanceStorage> ... KEY |-> VAL ... </instanceStorage>
+          ...
+        </contract>
+
+    rule [getContractData-other]:
+        <instrs> getContractData(DUR:Durability)
+              => allocObject(VAL)
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <hostStack> KEY : S => S </hostStack>
+        <callee> CONTRACT </callee>
+        <contractData> ... #skey(CONTRACT, DUR, KEY) |-> VAL ... </contractData>
+
+```
+
+## Helpers
+
+```k
+    syntax StorageType ::= Int2StorageType(Int)   [function, total]
+ // -------------------------------------------------------------------------------
+    rule Int2StorageType(0) => #temporary
+    rule Int2StorageType(1) => #persistent
+    rule Int2StorageType(_) => #instance      [owise]
+
+    syntax Bool ::= Int2StorageTypeValid(Int)   [function, total]
+ // ------------------------------------------------------------
+    rule Int2StorageTypeValid(I) => 0 <=Int I andBool I <=Int 2
+
+endmodule
+```