Remaining host functions for FxDAO: 5/11 (#43)

* implement `get_ledger_timestamp` and setter cheatcode * add timestamp tests * implement `del_contract_data` * add storage remove komet tests * implement `vec_(get|len|push_back)` * add wast tests for vector operations * add komet test for vector operations * Set Version: 0.1.38 --------- Co-authored-by: devops <[email protected]>
runtimeverification · Nov 5, 2024 · c94a4be · c94a4be
1 parent 0e50207
commit c94a4be
Show file tree

Hide file tree

Showing 13 changed files with 556 additions and 14 deletions.
diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.37
+0.1.38
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.37"
+version = "0.1.38"
 description = "K tooling for the Soroban platform"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/src/komet/kdist/soroban-semantics/cheatcodes.md b/src/komet/kdist/soroban-semantics/cheatcodes.md
@@ -34,6 +34,37 @@ module CHEATCODES
       requires getTag(HostVal(NEW_SEQ_NUM)) ==Int getTag(U32(0)) // check `NEW_SEQ_NUM` is a U32
 ```
 
+## kasmer_set_ledger_timestamp
+
+```rust
+    extern "C" {
+        fn kasmer_set_ledger_timestamp(x : u64);
+    }
+```
+
+```k
+    rule [kasmer-set-ledger-timestamp]:
+        <instrs> hostCall ( "env" , "kasmer_set_ledger_timestamp" , [ i64  .ValTypes ] -> [ .ValTypes ] )
+              => loadObject(HostVal(TIMESTAMP))
+              ~> setLedgerTimestamp
+              ~> toSmall(Void)
+                 ...
+        </instrs>
+        <locals>
+          0 |-> < i64 > TIMESTAMP // U64 HostVal
+        </locals>
+      requires getTag(HostVal(TIMESTAMP)) ==Int 6 // check `NEW_SEQ_NUM` is a U64
+        orBool getTag(HostVal(TIMESTAMP)) ==Int 64
+    
+    syntax InternalInstr ::= "setLedgerTimestamp"
+ // ---------------------------------------------
+    rule [setLedgerTimestamp]:
+        <instrs> setLedgerTimestamp => .K ... </instrs>
+        <hostStack> U64(TIMESTAMP) : S => S </hostStack>
+        <ledgerTimestamp> _ => TIMESTAMP </ledgerTimestamp>
+
+```
+
 ## kasmer_create_contract
 
 ```rust

diff --git a/src/komet/kdist/soroban-semantics/configuration.md b/src/komet/kdist/soroban-semantics/configuration.md
@@ -81,6 +81,7 @@ module CONFIG
 
 ```k
         <ledgerSequenceNumber> 0 </ledgerSequenceNumber>
+        <ledgerTimestamp> 0 </ledgerTimestamp>
         <logging> .List </logging>
       </soroban>
 

diff --git a/src/komet/kdist/soroban-semantics/host/context.md b/src/komet/kdist/soroban-semantics/host/context.md
@@ -61,6 +61,21 @@ Return the current ledger sequence number as `U32`.
         <ledgerSequenceNumber> SEQ_NUM </ledgerSequenceNumber>
 ```
 
+## get_ledger_timestamp
+
+Return the current ledger timestamp as `U64`.
+
+```k
+    rule [hostfun-get-ledger-timestamp]:
+        <instrs> hostCall ( "x" , "4" , [ .ValTypes ] -> [ i64  .ValTypes ] )
+              => allocObject(U64(TIMESTAMP))
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <locals> .Map </locals>
+        <ledgerTimestamp> TIMESTAMP </ledgerTimestamp>
+```
+
 ## fail_with_error
 
 ```k

diff --git a/src/komet/kdist/soroban-semantics/host/ledger.md b/src/komet/kdist/soroban-semantics/host/ledger.md
@@ -31,7 +31,7 @@ module HOST-LEDGER
         <instrs> putContractData(#instance) => toSmall(Void) ... </instrs>
         <hostStack> KEY : VAL : S => S </hostStack>
         <callee> CONTRACT </callee>
-        <contract> 
+        <contract>
           <contractId> CONTRACT </contractId>
           <instanceStorage> STORAGE => STORAGE [ KEY <- VAL ] </instanceStorage>
           ...
@@ -71,7 +71,7 @@ module HOST-LEDGER
         </instrs>
         <hostStack> KEY : S => S </hostStack>
         <callee> CONTRACT </callee>
-        <contract> 
+        <contract>
           <contractId> CONTRACT </contractId>
           <instanceStorage> STORAGE </instanceStorage>
           ...
@@ -112,7 +112,7 @@ module HOST-LEDGER
         </instrs>
         <hostStack> KEY : S => S </hostStack>
         <callee> CONTRACT </callee>
-        <contract> 
+        <contract>
           <contractId> CONTRACT </contractId>
           <instanceStorage> ... KEY |-> VAL ... </instanceStorage>
           ...
@@ -130,6 +130,43 @@ module HOST-LEDGER
 
 ```
 
+## del_contract_data
+
+```k
+    rule [hostfun-del-contract-data]:
+        <instrs> hostCall ( "l" , "2" , [ i64  i64  .ValTypes ] -> [ i64  .ValTypes ] )
+              => loadObjectFull(HostVal(KEY))
+              ~> delContractData(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 ::= delContractData(StorageType)   [symbol(delContractData)]
+ // ---------------------------------------------------------------------------------
+    rule [delContractData-instance]:
+        <instrs> delContractData(#instance) => toSmall(Void) ... </instrs>
+        <hostStack> KEY : S => S </hostStack>
+        <callee> CONTRACT </callee>
+        <contract>
+          <contractId> CONTRACT </contractId>
+          <instanceStorage> MAP => MAP [ KEY <- undef ] </instanceStorage>
+          ...
+        </contract>
+      requires KEY in_keys(MAP)
+
+    rule [delContractData-other]:
+        <instrs> delContractData(DUR:Durability) => toSmall(Void) ... </instrs>
+        <hostStack> KEY : S => S </hostStack>
+        <callee> CONTRACT </callee>
+        <contractData> MAP => MAP [#skey(CONTRACT, DUR, KEY) <- undef ] </contractData>
+      requires #skey(CONTRACT, DUR, KEY) in_keys(MAP)
+
+```
+
 ## extend_current_contract_instance_and_code_ttl
 
 ```k

diff --git a/src/komet/kdist/soroban-semantics/host/vector.md b/src/komet/kdist/soroban-semantics/host/vector.md
@@ -24,6 +24,86 @@ module HOST-VECTOR
         <locals> .Map </locals>
 ```
 
+## vec_get
+
+```k
+    rule [hostfun-vec-get]:
+        <instrs> hostCall ( "v" , "1" , [ i64  i64  .ValTypes ] -> [ i64  .ValTypes ] )
+              => loadObject(HostVal(INDEX))
+              ~> loadObject(HostVal(VEC))
+              ~> vecGet
+                 ...
+        </instrs>
+        <locals>
+          0 |-> < i64 > VEC
+          1 |-> < i64 > INDEX
+        </locals>
+
+    syntax InternalInstr ::= "vecGet"   [symbol(vecGet)]
+ // ----------------------------------------------------
+    rule [vecGet]:
+        <instrs> vecGet => VEC {{ I }} orDefault HostVal(0) ... </instrs> // use 'orDefault' to avoid non-total list lookup
+        <hostStack> ScVec(VEC) : U32(I) : S => S </hostStack>
+      requires 0 <=Int I
+       andBool I <Int size(VEC)
+
+```
+
+## vec_len
+
+```k
+    rule [hostfun-vec-len]:
+        <instrs> hostCall ( "v" , "3" , [ i64  .ValTypes ] -> [ i64  .ValTypes ] )
+              => loadObject(HostVal(VEC))
+              ~> vecLen
+                 ...
+        </instrs>
+        <locals>
+          0 |-> < i64 > VEC
+        </locals>
+
+    syntax InternalInstr ::= "vecLen"   [symbol(vecLen)]
+ // ----------------------------------------------------
+    rule [vecLen]:
+        <instrs> vecLen => toSmall(U32(size(VEC))) ... </instrs>
+        <hostStack> ScVec(VEC) : S => S </hostStack>
+
+```
+
+## vec_push_back
+
+Creates a new vector by appending a given item to the end of the provided vector.
+This function does not modify the original vector, maintaining immutability.
+Returns a new vector with the appended item.
+
+```k
+    rule [hostfun-vec-push-back]:
+        <instrs> hostCall ( "v" , "6" , [ i64  i64  .ValTypes ] -> [ i64  .ValTypes ] )
+              => loadObject(HostVal(VEC))
+              ~> vecPushBack(HostVal(ITEM))
+                 ...
+        </instrs>
+        <locals>
+          0 |-> < i64 > VEC
+          1 |-> < i64 > ITEM
+        </locals>
+
+    syntax InternalInstr ::= vecPushBack(HostVal)   [symbol(vecPushBack)]
+ // ----------------------------------------------------
+    rule [vecPushBack]:
+        <instrs> vecPushBack(ITEM)
+              => allocObject(
+                  ScVec(
+                    VEC ListItem(rel2abs(RELS, ITEM))
+                  )
+                 )
+              ~> returnHostVal
+              ...
+        </instrs>
+        <hostStack> ScVec(VEC) : S => S </hostStack>
+        <relativeObjects> RELS </relativeObjects>
+```
+
 ## vec_unpack_to_linear_memory
 
 ```k

diff --git a/src/tests/integration/data/soroban/contracts/test_containers/Cargo.toml b/src/tests/integration/data/soroban/contracts/test_containers/Cargo.toml
@@ -0,0 +1,15 @@
+[package]
+name = "test_containers"
+version = "0.0.0"
+edition = "2021"
+publish = false
+
+[lib]
+crate-type = ["cdylib"]
+doctest = false
+
+[dependencies]
+soroban-sdk = { workspace = true }
+
+[dev-dependencies]
+soroban-sdk = { workspace = true, features = ["testutils"] }
diff --git a/src/tests/integration/data/soroban/contracts/test_containers/src/lib.rs b/src/tests/integration/data/soroban/contracts/test_containers/src/lib.rs
@@ -0,0 +1,29 @@
+#![no_std]
+use soroban_sdk::{contract, contractimpl, Env, Vec};
+
+#[contract]
+pub struct ContainersContract;
+
+#[contractimpl]
+impl ContainersContract {
+
+    pub fn test_vector(env: Env, n: u32) -> bool {
+        let n = n % 100;
+
+        let mut vec: Vec<u32> = Vec::new(&env);
+        assert_eq!(vec.len(), 0);
+
+        for i in 0..n {
+            vec.push_back(i);
+        }
+
+        assert_eq!(vec.len(), n);
+
+        for i in 0..n {
+            assert_eq!(vec.get_unchecked(i), i);
+        }
+
+        true
+    }
+
+}
diff --git a/src/tests/integration/data/soroban/contracts/test_storage/src/lib.rs b/src/tests/integration/data/soroban/contracts/test_storage/src/lib.rs
@@ -23,11 +23,37 @@ impl StorageContract {
     }
 
     pub fn test_u32_overwrite(env: Env, num1: u32, num2: u32) -> bool {
-      env.storage().instance().set(&INST_KEY, &num1);
-      env.storage().instance().set(&INST_KEY, &num2);
-
-      let num: u32 = env.storage().instance().get(&INST_KEY).unwrap();
-
-      num == num2
-  }
+        env.storage().instance().set(&INST_KEY, &num1);
+        env.storage().instance().set(&INST_KEY, &num2);
+
+        let num: u32 = env.storage().instance().get(&INST_KEY).unwrap();
+
+        num == num2
+    }
+
+    pub fn test_set_remove_u64(env: Env, x: u64) -> bool {
+        // instance storage
+        env.storage().instance().set(&INST_KEY, &x);
+        assert!(env.storage().instance().has(&INST_KEY));
+
+        env.storage().instance().remove(&INST_KEY);
+        assert!(!env.storage().instance().has(&INST_KEY));
+
+        // temporary storage
+        env.storage().temporary().set(&TEMP_KEY, &x);
+        assert!(env.storage().temporary().has(&TEMP_KEY));
+
+        env.storage().temporary().remove(&TEMP_KEY);
+        assert!(!env.storage().temporary().has(&TEMP_KEY));
+
+
+        // persistent storage
+        env.storage().persistent().set(&PRST_KEY, &x);
+        assert!(env.storage().persistent().has(&PRST_KEY));
+
+        env.storage().persistent().remove(&PRST_KEY);
+        assert!(!env.storage().persistent().has(&PRST_KEY));
+
+        true
+    }
 }
diff --git a/src/tests/integration/data/soroban/contracts/test_ttl/src/lib.rs b/src/tests/integration/data/soroban/contracts/test_ttl/src/lib.rs
@@ -1,11 +1,15 @@
 #![no_std]
-use soroban_sdk::{contract, contractimpl, Env, Val};
+use soroban_sdk::{contract, contractimpl, Env, FromVal, Val};
 
 #[contract]
 pub struct TtlContract;
 
 extern "C" {
+
     fn kasmer_set_ledger_sequence(x : u64);
+
+    fn kasmer_set_ledger_timestamp(x : u64);
+
 }
 
 fn set_ledger_sequence(x: u32) {
@@ -14,6 +18,12 @@ fn set_ledger_sequence(x: u32) {
     }
 }
 
+fn set_ledger_timestamp(env: &Env, x: u64) {
+    unsafe {
+        kasmer_set_ledger_timestamp(Val::from_val(env, &x).get_payload());
+    }
+}
+
 #[contractimpl]
 impl TtlContract {
 
@@ -41,4 +51,10 @@ impl TtlContract {
         // Consider adding a custom hook to retrieve the TTL value for more thorough testing.
         true
     }
+
+    pub fn test_timestamp(env: Env, t: u64) -> bool {
+        set_ledger_timestamp(&env, t);
+        env.ledger().timestamp() == t
+    }
+
 }