Implement contract TTL extension functions (#24)

* Add live-until cells for contracts and code * Implement extend ttl host functions * add test * Set Version: 0.1.17 * add fuzz test * fix side conditions and refactor --------- Co-authored-by: devops <[email protected]>
runtimeverification · Aug 9, 2024 · 0b2d0f2 · 0b2d0f2
1 parent 05c4936
commit 0b2d0f2
Show file tree

Hide file tree

Showing 10 changed files with 261 additions and 10 deletions.
diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.16
+0.1.17
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.16"
+version = "0.1.17"
 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
@@ -45,6 +45,12 @@ module CONFIG
 
 ```k
             <instanceStorage> .Map </instanceStorage> // Map of ScVal to ScVal
+```
+
+- `contractLiveUntil`: The ledger sequence number until which the contract instance will live.
+
+```k
+            <contractLiveUntil> 0 </contractLiveUntil>
           </contract>
         </contracts>
         <accounts>
@@ -60,7 +66,13 @@ module CONFIG
 
 ```k
         <contractData> .Map </contractData> // Map of StorageKey to ScVal
-        <contractCodes> .Map </contractCodes>
+        <contractCodes>
+          <contractCode multiplicity="*" type="Map">
+            <codeHash>      .Bytes         </codeHash>
+            <codeLiveUntil> 0              </codeLiveUntil>
+            <codeWasm>      #emptyModule() </codeWasm> 
+          </contractCode>
+        </contractCodes>
 ```
 
 - `ledgerSequenceNumber`: The current block (or "ledger" in Stellar) number.

diff --git a/src/ksoroban/kdist/soroban-semantics/host/ledger.md b/src/ksoroban/kdist/soroban-semantics/host/ledger.md
@@ -130,6 +130,83 @@ module HOST-LEDGER
 
 ```
 
+## extend_current_contract_instance_and_code_ttl
+
+```k
+    rule [hostfun-extend-current-contract-instance-and-code-ttl]:
+        <instrs> hostCall ( "l" , "8" , [ i64  i64  .ValTypes ] -> [ i64  .ValTypes ] )
+              => loadObject(HostVal(EXTEND_TO))
+              ~> loadObject(HostVal(THRESHOLD))
+              ~> extendContractTtl(CONTRACT)
+              ~> loadObject(HostVal(EXTEND_TO))
+              ~> loadObject(HostVal(THRESHOLD))
+              ~> extendContractCodeTtl(CONTRACT)
+              ~> toSmall(Void)
+                 ...
+        </instrs>
+        <locals>
+          0 |-> < i64 > THRESHOLD   // U32
+          1 |-> < i64 > EXTEND_TO   // U32
+        </locals>
+        <callee> CONTRACT </callee>
+
+  // If the TTL for the contract is less than or equal to `THRESHOLD`,
+  // update <contractLiveUntil>
+    syntax InternalInstr ::= extendContractTtl(ContractId)   [symbol(extendContractTtl)]
+ // -------------------------------------------------------------------------------
+    rule [extendContractTtl]:
+        <instrs> extendContractTtl(CONTRACT) => .K ... </instrs>
+        <hostStack> U32(THRESHOLD) : U32(EXTEND_TO) : S => S </hostStack>
+        <contract>
+          <contractId> CONTRACT </contractId>
+          <contractLiveUntil> LIVE_UNTIL
+                           => extendedLiveUntil(SEQ, LIVE_UNTIL, THRESHOLD, EXTEND_TO)
+          </contractLiveUntil>
+          ...
+        </contract>
+        <ledgerSequenceNumber> SEQ </ledgerSequenceNumber>
+      requires THRESHOLD <=Int EXTEND_TO   // input is valid
+       andBool SEQ <=Int LIVE_UNTIL        // entry is still alive
+
+    syntax Int ::= extendedLiveUntil(Int, Int, Int, Int)    [function, total]
+ // -----------------------------------------------------------------------------------
+    rule extendedLiveUntil(SEQ, LIVE_UNTIL, THRESHOLD, EXTEND_TO) => SEQ +Int EXTEND_TO
+      requires LIVE_UNTIL -Int SEQ <=Int THRESHOLD            // CURRENT_TTL <= THRESHOLD
+       andBool LIVE_UNTIL          <Int  SEQ +Int EXTEND_TO   // LIVE_UNTIL  <  NEW_LIVE_UNTIL
+
+    rule extendedLiveUntil(_, LIVE_UNTIL, _, _) => LIVE_UNTIL
+      [owise]
+
+    syntax InternalInstr ::= extendContractCodeTtl(ContractId)   [symbol(extendContractCodeTtl)]
+ // --------------------------------------------------------------------------------------------
+    rule [extendContractCodeTtl]:
+        <instrs> extendContractCodeTtl(CONTRACT) => extendCodeTtl(HASH) ... </instrs>
+        <contract>
+          <contractId> CONTRACT </contractId>
+          <wasmHash> HASH </wasmHash>
+          ...
+        </contract>
+
+  // If the TTL for the contract code is less than `THRESHOLD`, update contractLiveUntil
+  //    where TTL is defined as LIVE_UNTIL - SEQ.
+    syntax InternalInstr ::= extendCodeTtl(Bytes)   [symbol(extendCodeTtl)]
+ // -------------------------------------------------------------------------------
+    rule [extendCodeTtl]:
+        <instrs> extendCodeTtl(HASH) => .K ... </instrs>
+        <hostStack> U32(THRESHOLD) : U32(EXTEND_TO) : S => S </hostStack>
+        <contractCode>
+          <codeHash> HASH </codeHash>
+          <codeLiveUntil> LIVE_UNTIL
+                       => extendedLiveUntil(SEQ, LIVE_UNTIL, THRESHOLD, EXTEND_TO)
+          </codeLiveUntil>
+          ...
+        </contractCode>
+        <ledgerSequenceNumber> SEQ </ledgerSequenceNumber>
+      requires THRESHOLD <=Int EXTEND_TO   // input is valid
+       andBool SEQ <=Int LIVE_UNTIL        // entry is still alive
+
+```
+
 ## Helpers
 
 ```k

diff --git a/src/ksoroban/kdist/soroban-semantics/kasmer.md b/src/ksoroban/kdist/soroban-semantics/kasmer.md
@@ -86,15 +86,19 @@ module KASMER
       [priority(55)]
 
 //  ----------------------------------------------------------------------------
-    rule [uploadWasm]:
-        <k> uploadWasm(HASH, MOD) => .K ... </k>
-        <contractCodes> MODS => MODS [ HASH <- MOD ] </contractCodes>
-      requires notBool( HASH in_keys(MODS) )
 
     rule [uploadWasm-exists]:
         <k> uploadWasm(HASH, _MOD) => .K ... </k>
-        <contractCodes> MODS </contractCodes>
-      requires HASH in_keys(MODS)
+        <codeHash> HASH </codeHash>  
+      
+    rule [uploadWasm]:
+        <k> uploadWasm(HASH, MOD) => .K ... </k>
+        (.Bag => <contractCode>
+          <codeHash> HASH </codeHash>
+          <codeWasm> MOD </codeWasm>
+          ...
+        </contractCode>)
+      [priority(51)]
 
  // -----------------------------------------------------------------------------------------------------------------------
     rule [deployContract-existing]:

diff --git a/src/ksoroban/kdist/soroban-semantics/soroban.md b/src/ksoroban/kdist/soroban-semantics/soroban.md
@@ -49,7 +49,11 @@ module SOROBAN
           <wasmHash> HASH </wasmHash>
           ...
         </contract>
-        <contractCodes> ... HASH |-> CODE:ModuleDecl ... </contractCodes>
+        <contractCode>
+          <codeHash> HASH </codeHash>
+          <codeWasm> CODE </codeWasm>
+          ...
+        </contractCode>
         <instrs> .K </instrs>
 
     // rule [callContractAux-not-contract]:

diff --git a/src/tests/integration/data/extend_ttl.wast b/src/tests/integration/data/extend_ttl.wast
@@ -0,0 +1,77 @@
+
+setExitCode(1)
+
+uploadWasm( b"test-wasm",
+;; #![no_std]
+;; use soroban_sdk::{contract, contractimpl, Env};
+;; 
+;; #[contract]
+;; pub struct IncrementContract;
+;; 
+;; #[contractimpl]
+;; impl IncrementContract {
+;;     pub fn extend_ttl(env: Env, threshold: u32, extend_to: u32) {
+;;         env.storage().instance().extend_ttl(threshold, extend_to);
+;;     }
+;; }
+(module $soroban_increment_contract.wasm
+  (type (;0;) (func (param i64 i64) (result i64)))
+  (type (;1;) (func))
+  (import "l" "8" (func $_ZN17soroban_env_guest5guest6ledger45extend_current_contract_instance_and_code_ttl17h6e6604048593c195E (type 0)))
+  (func $extend_ttl (type 0) (param i64 i64) (result i64)
+    block  ;; label = @1
+      local.get 0
+      i64.const 255
+      i64.and
+      i64.const 4
+      i64.ne
+      br_if 0 (;@1;)
+      local.get 1
+      i64.const 255
+      i64.and
+      i64.const 4
+      i64.ne
+      br_if 0 (;@1;)
+      local.get 0
+      i64.const -4294967292
+      i64.and
+      local.get 1
+      i64.const -4294967292
+      i64.and
+      call $_ZN17soroban_env_guest5guest6ledger45extend_current_contract_instance_and_code_ttl17h6e6604048593c195E
+      drop
+      i64.const 2
+      return
+    end
+    unreachable
+    unreachable)
+  (func $_ (type 1))
+  (memory (;0;) 16)
+  (global $__stack_pointer (mut i32) (i32.const 1048576))
+  (global (;1;) i32 (i32.const 1048576))
+  (global (;2;) i32 (i32.const 1048576))
+  (export "memory" (memory 0))
+  (export "extend_ttl" (func $extend_ttl))
+  (export "_" (func $_))
+  (export "__data_end" (global 1))
+  (export "__heap_base" (global 2)))
+)
+
+setAccount(Account(b"test-account"), 9876543210)
+
+deployContract(
+  Account(b"test-account"),
+  Contract(b"test-sc"),
+  b"test-wasm",
+  .List
+)
+
+callTx(
+  Account(b"test-caller"),
+  Contract(b"test-sc"),
+  "extend_ttl",
+  ListItem(U32(100)) ListItem(U32(100)),
+  Void
+)
+
+setExitCode(0)
diff --git a/src/tests/integration/data/soroban/contracts/test_ttl/Cargo.toml b/src/tests/integration/data/soroban/contracts/test_ttl/Cargo.toml
@@ -0,0 +1,15 @@
+[package]
+name = "test_ttl"
+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_ttl/README.md b/src/tests/integration/data/soroban/contracts/test_ttl/README.md
@@ -0,0 +1,18 @@
+A quick example of a contract that can be ran with `ksoroban test`
+
+You will need to have the stellar cli utils installed:
+https://developers.stellar.org/docs/build/smart-contracts/getting-started/setup
+
+And the soroban semantics kompiled:
+```
+kdist build soroban-semantics.llvm
+```
+
+And then (from this directory):
+
+```sh
+soroban contract build --out-dir output
+ksoroban test output/test_adder.wasm
+```
+
+`ksoroban test` should exit successfully
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
@@ -0,0 +1,44 @@
+#![no_std]
+use soroban_sdk::{contract, contractimpl, Env, Val};
+
+#[contract]
+pub struct TtlContract;
+
+extern "C" {
+    fn kasmer_set_ledger_sequence(x : u64);
+}
+
+fn set_ledger_sequence(x: u32) {
+    unsafe {
+        kasmer_set_ledger_sequence(Val::from_u32(x).to_val().get_payload());
+    }
+}
+
+#[contractimpl]
+impl TtlContract {
+
+    pub fn test_ttl(
+        env: Env,
+        init_live_until: 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);
+
+        // When:
+            env.storage().instance().extend_ttl(threshold, extend_to);
+        }
+
+        // Since there is no getter function for the TTL value, we cannot verify 
+        // if `extend_ttl` works as expected.
+        // Currently, we only check if the function runs without errors.
+        // Consider adding a custom hook to retrieve the TTL value for more thorough testing.
+        true
+    }
+}