Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remaining host functions for FxDAO: 5/11 #43

Merged
merged 8 commits into from
Nov 5, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion package/version
Original file line number Diff line number Diff line change
@@ -1 +1 @@
0.1.37
0.1.38
2 changes: 1 addition & 1 deletion pyproject.toml
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.37"
version = "0.1.38"
description = "K tooling for the Soroban platform"
authors = [
"Runtime Verification, Inc. <[email protected]>",
Expand Down
31 changes: 31 additions & 0 deletions src/komet/kdist/soroban-semantics/cheatcodes.md
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@bbyalcinkaya, could you please elaborate a bit on the presence of toSmall at the end of the rewriting operation? After going through its implementation, it is not immediately clear to me why we should leave it at the K cell at the end of certain operations.

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

My current understanding is that it is working as some sort of a return value for this host function (as in it is returning nothing, in this case), but I'd like to double check.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@ACassimiro That's correct, it is used as a return value here. toSmall converts ScVals to HostVals. When a HostVal is on top of the <instrs> cell, it is executed as i64.const _ instruction: rule.

...
</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
Expand Down
1 change: 1 addition & 0 deletions src/komet/kdist/soroban-semantics/configuration.md
Original file line number Diff line number Diff line change
Expand Up @@ -81,6 +81,7 @@ module CONFIG

```k
<ledgerSequenceNumber> 0 </ledgerSequenceNumber>
<ledgerTimestamp> 0 </ledgerTimestamp>
<logging> .List </logging>
</soroban>

Expand Down
15 changes: 15 additions & 0 deletions src/komet/kdist/soroban-semantics/host/context.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
43 changes: 40 additions & 3 deletions src/komet/kdist/soroban-semantics/host/ledger.md
Original file line number Diff line number Diff line change
Expand Up @@ -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>
...
Expand Down Expand Up @@ -71,7 +71,7 @@ module HOST-LEDGER
</instrs>
<hostStack> KEY : S => S </hostStack>
<callee> CONTRACT </callee>
<contract>
<contract>
<contractId> CONTRACT </contractId>
<instanceStorage> STORAGE </instanceStorage>
...
Expand Down Expand Up @@ -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>
...
Expand All @@ -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
Expand Down
80 changes: 80 additions & 0 deletions src/komet/kdist/soroban-semantics/host/vector.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@bbyalcinkaya could you please elaborate on how orDefault operates here? And how it is used to avoid a scenario of non-total list lookup? I'm not entirely familiar with this production, so if you have a reference for me to take a deeper look into it, it would be more than enough.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It is a typed and total list lookup defined here. It returns the default value if the index is out of bounds or the list item at that index is not a HostVal.

I could've used the normal list lookup but that would require:

  1. projection cast on the list lookup result because _ [_] returns KItem: {VEC[I]}:>HostVal
  2. side condition to check the list item sort: isHostVal(VEC[I])
  3. preserves-definedness attribute to avoid booster backend fallbacks (and manually check if it actually does)

<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
Expand Down
Original file line number Diff line number Diff line change
@@ -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"] }
Original file line number Diff line number Diff line change
@@ -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
}

}
Original file line number Diff line number Diff line change
Expand Up @@ -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
}
}
18 changes: 17 additions & 1 deletion src/tests/integration/data/soroban/contracts/test_ttl/src/lib.rs
Original file line number Diff line number Diff line change
@@ -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) {
Expand All @@ -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 {

Expand Down Expand Up @@ -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
}

}
Loading
Loading