Skip to content

Commit

Permalink
Implement Contract Upgrade and TTL Management Host Functions (#47)
Browse files Browse the repository at this point in the history 
* fix `getTag(SCBool(_))`

* implement `update_current_contract_wasm` and add a wast test

* add live-until field to storage entries

* implement `extend_contract_data_ttl`

* add `storage.wast` tests

* update `test_ttl` after introducing `#maxEntryTtl`

* Set Version: 0.1.39

* Set Version: 0.1.41

---------

Co-authored-by: devops <[email protected]>
  • Loading branch information
@bbyalcinkaya
bbyalcinkaya and devops authored Nov 19, 2024
1 parent 3b9a1d9 commit 50117c0
Show file tree
Hide file tree
Showing 8 changed files with 323 additions and 17 deletions.
2 changes: 1 addition & 1 deletion package/version
View file
Original file line number Diff line number Diff line change
@@ -1 +1 @@
0.1.40
0.1.41
2 changes: 1 addition & 1 deletion pyproject.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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]>",
Expand Down
12 changes: 11 additions & 1 deletion src/komet/kdist/soroban-semantics/configuration.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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>
Expand Down Expand Up @@ -99,6 +99,8 @@ module CONFIG
syntax StorageKey ::= #skey( ContractId , Durability , ScVal ) [symbol(StorageKey)]
syntax StorageVal ::= #sval( ScVal , Int ) [symbol(StorageVal)]
endmodule
```

Expand Down Expand Up @@ -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
```
4 changes: 2 additions & 2 deletions src/komet/kdist/soroban-semantics/data.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
112 changes: 108 additions & 4 deletions src/komet/kdist/soroban-semantics/host/ledger.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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>
```

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
```
28 changes: 20 additions & 8 deletions src/tests/integration/data/soroban/contracts/test_ttl/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
121 changes: 121 additions & 0 deletions src/tests/integration/data/storage.wast
View file
Original file line number Diff line number Diff line change
@@ -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)
Loading

0 comments on commit 50117c0

Please sign in to comment.