Implement Contract Upgrade and TTL Management Host Functions

package/version

@@ -1 +1 @@
-0.1.40
+0.1.41

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "komet"
-version = "0.1.40"
+version = "0.1.41"
 description = "K tooling for the Soroban platform"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/komet/kdist/soroban-semantics/configuration.md

@@ -65,7 +65,7 @@ module CONFIG
     Keys and values must be fully resolved `ScVal`s as in `<instanceStorage>`.
 
 ```k
-        <contractData> .Map </contractData> // Map of StorageKey to ScVal
+        <contractData> .Map </contractData> // Map of StorageKey to StorageVal
         <contractCodes>
           <contractCode multiplicity="*" type="Map">
             <codeHash>      .Bytes         </codeHash>
@@ -99,6 +99,8 @@ module CONFIG
 
     syntax StorageKey ::= #skey( ContractId , Durability , ScVal )   [symbol(StorageKey)]
 
+    syntax StorageVal ::= #sval( ScVal , Int )                       [symbol(StorageVal)]
+
 endmodule
 ```
 
@@ -470,6 +472,14 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly
 
 ```
 
+## Exception throwing
+
 ```k
+    syntax InternalInstr ::= #throw(ErrorType, Int)    [symbol(throw)]
+ // ------------------------------------------------------------------
+    rule [throw]:
+        <instrs> #throw(ERRTYPE, CODE) ~> _REST => .K </instrs>
+        <hostStack> S => Error(ERRTYPE, CODE) : S </hostStack>
+
 endmodule
 ```

src/komet/kdist/soroban-semantics/data.md

@@ -143,8 +143,8 @@ module HOST-OBJECT
   // https://github.com/stellar/stellar-protocol/blob/master/core/cap-0046-01.md#tag-values
     syntax Int ::= getTag(ScVal)   [function, total]
  // -----------------------------------------------------
-    rule getTag(SCBool(true))  => 0
-    rule getTag(SCBool(false)) => 1
+    rule getTag(SCBool(false)) => 0
+    rule getTag(SCBool(true))  => 1
     rule getTag(Void)          => 2
     rule getTag(Error(_,_))    => 3
     rule getTag(U32(_))        => 4

src/komet/kdist/soroban-semantics/host/ledger.md

@@ -37,14 +37,26 @@ module HOST-LEDGER
           ...
         </contract>
 
-    rule [putContractData-other]:
+    rule [putContractData-other-existing]:
         <instrs> putContractData(DUR:Durability) => toSmall(Void) ... </instrs>
         <hostStack> KEY : VAL : S => S </hostStack>
         <callee> CONTRACT </callee>
         <contractData>
-          STORAGE => STORAGE [ #skey(CONTRACT, DUR, KEY) <- VAL ]
+          ...
+          #skey(CONTRACT, DUR, KEY) |-> #sval(_ => VAL, _LIVE_UNTIL)
+          ...
         </contractData>
 
+    rule [putContractData-other-new]:
+        <instrs> putContractData(DUR:Durability) => toSmall(Void) ... </instrs>
+        <hostStack> KEY : VAL : S => S </hostStack>
+        <callee> CONTRACT </callee>
+        <contractData>
+          STORAGE => STORAGE [ #skey(CONTRACT, DUR, KEY) <- #sval(VAL, minLiveUntil(DUR, SEQ)) ]
+        </contractData>
+        <ledgerSequenceNumber> SEQ </ledgerSequenceNumber>
+      requires notBool( #skey(CONTRACT, DUR, KEY) in_keys(STORAGE) )
+
 ```
 
 ## has_contract_data
@@ -126,7 +138,7 @@ module HOST-LEDGER
         </instrs>
         <hostStack> KEY : S => S </hostStack>
         <callee> CONTRACT </callee>
-        <contractData> ... #skey(CONTRACT, DUR, KEY) |-> VAL ... </contractData>
+        <contractData> ... #skey(CONTRACT, DUR, KEY) |-> #sval(VAL, _) ... </contractData>
 
 ```
 
@@ -165,6 +177,83 @@ module HOST-LEDGER
         <contractData> MAP => MAP [#skey(CONTRACT, DUR, KEY) <- undef ] </contractData>
       requires #skey(CONTRACT, DUR, KEY) in_keys(MAP)
 
+```
+## update_current_contract_wasm
+
+```k
+    rule [hostfun-update-current-contract-wasm]:
+        <instrs> hostCall ( "l" , "6" , [ i64  .ValTypes ] -> [ i64  .ValTypes ] )
+              => loadObject(HostVal(HASH))
+              ~> updateContractWasm(CALLEE)
+              ~> toSmall(Void)
+                 ...
+        </instrs>
+        <locals>
+          0 |-> < i64 > HASH   // Bytes
+        </locals>
+        <callee> CALLEE </callee>
+
+    syntax InternalInstr ::= updateContractWasm(ContractId)   [symbol(updateContractWasm)]
+ // --------------------------------------------------------------------------------------
+    rule [updateContractWasm]:
+        <instrs> updateContractWasm(CONTRACT) => .K ... </instrs>
+        <hostStack> ScBytes(HASH) : S => S </hostStack>
+        <contract>
+          <contractId> CONTRACT </contractId>
+          <wasmHash> _ => HASH </wasmHash>
+          ...
+        </contract>
+        <contractCode>
+          <codeHash> HASH </codeHash>
+          ...
+        </contractCode>
+
+```
+
+## extend_contract_data_ttl
+
+```k
+    rule [hostfun-extend-contract-data-ttl]:
+        <instrs> hostCall ( "l" , "7" , [ i64  i64  i64  i64 .ValTypes ] -> [ i64  .ValTypes ] )
+              => loadObject(HostVal(EXTEND_TO))
+              ~> loadObject(HostVal(THRESHOLD))
+              ~> loadObjectFull(HostVal(KEY))
+              ~> extendContractDataTtl(CONTRACT, Int2StorageType(STORAGE_TYPE))
+              ~> toSmall(Void)
+                 ...
+        </instrs>
+        <locals>
+          0 |-> < i64 > KEY            // HostVal
+          1 |-> < i64 > STORAGE_TYPE   // 0: temp, 1: persistent, 2: instance
+          2 |-> < i64 > THRESHOLD   // U32
+          3 |-> < i64 > EXTEND_TO   // U32
+        </locals>
+        <callee> CONTRACT </callee>
+      requires Int2StorageTypeValid(STORAGE_TYPE)
+
+    syntax InternalInstr ::= extendContractDataTtl(ContractId, StorageType)   [symbol(extendContractDataTtl)]
+ // --------------------------------------------------------------------------------------------
+    rule [extendContractDataTtl]:
+        <instrs> extendContractDataTtl(CONTRACT, DUR:Durability) => .K ... </instrs>
+        <hostStack> KEY:ScVal : U32(THRESHOLD) : U32(EXTEND_TO) : S => S </hostStack>
+        <contractData>
+          ...
+          #skey(CONTRACT, DUR, KEY)
+            |-> #sval(_VAL, LIVE_UNTIL => extendedLiveUntil(SEQ, LIVE_UNTIL, THRESHOLD, EXTEND_TO))
+          ... 
+        </contractData>
+        <ledgerSequenceNumber> SEQ </ledgerSequenceNumber>
+      requires THRESHOLD <=Int EXTEND_TO   // input is valid
+       andBool SEQ <=Int LIVE_UNTIL        // entry is alive
+       andBool ( DUR =/=K #temporary 
+          orBool extendedLiveUntil(SEQ, LIVE_UNTIL, THRESHOLD, EXTEND_TO) <=Int maxLiveUntil(SEQ)
+       ) // #temporary TTLs has to be exact
+
+    rule [extendContractDataTtl-err]:
+        <instrs> extendContractDataTtl(_CONTRACT, _TYP) => #throw(ErrStorage, InvalidAction) ... </instrs>
+        <hostStack> _KEY:ScVal : U32(_THRESHOLD) : U32(_EXTEND_TO) : S => S </hostStack>
+      [owise]
+
 ```
 
 ## extend_current_contract_instance_and_code_ttl
@@ -207,7 +296,8 @@ module HOST-LEDGER
 
     syntax Int ::= extendedLiveUntil(Int, Int, Int, Int)    [function, total]
  // -----------------------------------------------------------------------------------
-    rule extendedLiveUntil(SEQ, LIVE_UNTIL, THRESHOLD, EXTEND_TO) => SEQ +Int EXTEND_TO
+    rule extendedLiveUntil(SEQ, LIVE_UNTIL, THRESHOLD, EXTEND_TO)
+      => minInt( SEQ +Int EXTEND_TO , maxLiveUntil(SEQ) )
       requires LIVE_UNTIL -Int SEQ <=Int THRESHOLD            // CURRENT_TTL <= THRESHOLD
        andBool LIVE_UNTIL          <Int  SEQ +Int EXTEND_TO   // LIVE_UNTIL  <  NEW_LIVE_UNTIL
 
@@ -257,5 +347,19 @@ module HOST-LEDGER
  // ------------------------------------------------------------
     rule Int2StorageTypeValid(I) => 0 <=Int I andBool I <=Int 2
 
+  // make these values variable
+    syntax Int ::= minEntryTtl(Durability)   [function, total]
+                 | "#maxEntryTtl"            [macro]
+ // -------------------------------------------------
+    rule minEntryTtl(#temporary)  => 16 
+    rule minEntryTtl(#persistent) => 4096
+    rule #maxEntryTtl             => 6312000
+
+    syntax Int ::= minLiveUntil(Durability, Int)   [function, total]
+                 | maxLiveUntil(Int)               [function, total]
+ // -----------------------------------------------------------------------
+    rule minLiveUntil(DUR, SEQ) => SEQ +Int minEntryTtl(DUR) -Int 1
+    rule maxLiveUntil(SEQ)      => SEQ +Int #maxEntryTtl -Int 1
+
 endmodule
 ```

src/tests/integration/data/soroban/contracts/test_ttl/src/lib.rs

@@ -24,25 +24,37 @@ fn set_ledger_timestamp(env: &Env, x: u64) {
     }
 }
 
+const MAX_ENTRY_TTL: u32 = 6312000;
+
 #[contractimpl]
 impl TtlContract {
 
     pub fn test_ttl(
         env: Env,
-        init_live_until: u32,
+        ttl: u32,
         seq: u32,
         threshold: u32,
         extend_to: u32
     ) -> bool {
 
-        // Given:
-        //   contract is still alive and extend_ttl inputs are valid
-        if seq <= init_live_until && threshold <= extend_to {
-            env.storage().instance().extend_ttl(0, init_live_until);
-            set_ledger_sequence(seq);
+        // Validate the input
+        if threshold > ttl || threshold > extend_to || ttl == 0 || extend_to == 0 {
+            return true;
+        }
+
+        // Set the initial TTL and ledger sequence number
+        env.storage().instance().extend_ttl(threshold, ttl);
+        let init_ttl = u32::min(ttl, MAX_ENTRY_TTL);
+        let init_seq = env.ledger().sequence();
+        let init_live_until = init_seq.checked_add(init_ttl - 1); // the sequence number at the beginning is 0
+
+        set_ledger_sequence(seq);
 
-        // When:
-            env.storage().instance().extend_ttl(threshold, extend_to);
+        if let Some(live_until) = init_live_until {
+            // If the contract is still alive extend the instance ttl
+            if seq <= live_until {
+                env.storage().instance().extend_ttl(threshold, extend_to);
+            }
         }
 
         // Since there is no getter function for the TTL value, we cannot verify 

src/tests/integration/data/storage.wast

@@ -0,0 +1,121 @@
+
+setExitCode(1)
+
+uploadWasm( b"test-wasm",
+(module $soroban_increment_contract.wasm
+  (import "l" "_" (func $put_contract_data        (param i64 i64 i64)     (result i64)))
+  (import "l" "0" (func $has_contract_data        (param i64 i64)         (result i64)))
+  (import "l" "1" (func $get_contract_data        (param i64 i64)         (result i64)))
+  (import "l" "2" (func $del_contract_data        (param i64 i64)         (result i64)))
+  (import "l" "7" (func $extend_contract_data_ttl (param i64 i64 i64 i64) (result i64)))
+
+  (func $storage_type (param i64) (result i64)
+    local.get 0
+    i64.const 32
+    i64.shr_u
+  )
+
+  (func $put (export "put") (param i64 i64 i64) (result i64)
+    (call $put_contract_data
+      (local.get 0)
+      (local.get 1)
+      (call $storage_type (local.get 2))
+    )
+  )
+
+  (func $has (export "has") (param i64 i64) (result i64)
+    (call $has_contract_data
+      (local.get 0)
+      (call $storage_type (local.get 1))
+    )
+  )
+
+  (func $get (export "get") (param i64 i64) (result i64)
+    (call $get_contract_data
+      (local.get 0)
+      (call $storage_type (local.get 1))
+    )
+  )
+
+  (func $del (export "del") (param i64 i64) (result i64)
+    (call $del_contract_data
+      (local.get 0)
+      (call $storage_type (local.get 1))
+    )
+  )
+
+
+  (func $extend_ttl (export "extend_ttl") (param i64 i64 i64 i64) (result i64)
+    (call $extend_contract_data_ttl
+      (local.get 0)
+      (call $storage_type (local.get 1))
+      (local.get 2)
+      (local.get 3)
+    )
+  )
+)
+)
+
+setAccount(Account(b"test-account"), 9876543210)
+
+deployContract( Account(b"test-account"), Contract(b"test-sc"), b"test-wasm" )
+
+;; Test put/has/get/del
+;; 1. has                           -> false
+;; 2. put "foo" U32(123456789) temp -> void
+;; 3. has "foo" temp                -> true
+;; 4. get "foo" temp                -> U32(123456789)
+;; 5. del "foo" temp                -> void
+;; 6. has "foo" temp                -> false
+
+callTx(
+  Account(b"test-caller"), Contract(b"test-sc"),
+  "has", ListItem(Symbol(str("foo"))) ListItem(U32(0)),
+  SCBool(false)
+)
+
+callTx(
+  Account(b"test-caller"), Contract(b"test-sc"),
+  "put", ListItem(Symbol(str("foo"))) ListItem(U32(123456789)) ListItem(U32(0)),
+  Void
+)
+
+callTx(
+  Account(b"test-caller"), Contract(b"test-sc"),
+  "has", ListItem(Symbol(str("foo"))) ListItem(U32(0)),
+  SCBool(true)
+)
+
+callTx(
+  Account(b"test-caller"), Contract(b"test-sc"),
+  "get", ListItem(Symbol(str("foo"))) ListItem(U32(0)),
+  U32(123456789)
+)
+
+callTx(
+  Account(b"test-caller"), Contract(b"test-sc"),
+  "del", ListItem(Symbol(str("foo"))) ListItem(U32(0)),
+  Void
+)
+
+callTx(
+  Account(b"test-caller"), Contract(b"test-sc"),
+  "has", ListItem(Symbol(str("foo"))) ListItem(U32(0)),
+  SCBool(false)
+)
+
+;; Test extend TTL
+callTx(
+  Account(b"test-caller"), Contract(b"test-sc"),
+  "put", ListItem(Symbol(str("foo"))) ListItem(U32(123456789)) ListItem(U32(0)),
+  Void
+)
+
+callTx(
+  Account(b"test-caller"), Contract(b"test-sc"),
+  "extend_ttl", ListItem(Symbol(str("foo"))) ListItem(U32(0)) ListItem(U32(100)) ListItem(U32(200)),
+  Void
+)
+
+
+setExitCode(0)