From 2c0fc8d9f368292a021fffadf9f884a1ec94429b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Burak=20Bilge=20Yal=C3=A7=C4=B1nkaya?= Date: Mon, 16 Sep 2024 23:41:53 +0300 Subject: [PATCH] Fix relative handles in containers (#38) * Add test: fxdao test_set_admin * Add python bindings for `SCAddress` * Set Version: 0.1.32 * Convert rel handles to abs when creating maps and vecs * Set Version: 0.1.34 --------- Co-authored-by: devops --- package/version | 2 +- pyproject.toml | 2 +- src/komet/kast/syntax.py | 4 ++ .../kdist/soroban-semantics/configuration.md | 20 ++++++++- src/komet/kdist/soroban-semantics/host/map.md | 3 +- .../kdist/soroban-semantics/host/vector.md | 9 +++- src/komet/scval.py | 43 +++++++++++++++++++ .../soroban/contracts/test_fxdao/src/lib.rs | 9 ++++ 8 files changed, 87 insertions(+), 5 deletions(-) diff --git a/package/version b/package/version index 50140e3..9dd1793 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.33 +0.1.34 diff --git a/pyproject.toml b/pyproject.toml index dc2c133..2983921 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "komet" -version = "0.1.33" +version = "0.1.34" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", diff --git a/src/komet/kast/syntax.py b/src/komet/kast/syntax.py index aaba07e..0b1cab3 100644 --- a/src/komet/kast/syntax.py +++ b/src/komet/kast/syntax.py @@ -95,6 +95,10 @@ def sc_bytes(b: bytes) -> KInner: return KApply('SCVal:Bytes', [token(b)]) +def sc_address(address: KInner) -> KInner: + return KApply('SCVal:Address', [address]) + + def sc_vec(l: Iterable[KInner]) -> KInner: return KApply('SCVal:Vec', list_of(l)) diff --git a/src/komet/kdist/soroban-semantics/configuration.md b/src/komet/kdist/soroban-semantics/configuration.md index 0748778..1c10a31 100644 --- a/src/komet/kdist/soroban-semantics/configuration.md +++ b/src/komet/kdist/soroban-semantics/configuration.md @@ -333,7 +333,7 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly rule [loadObject-rel]: loadObject(VAL) - => loadObject(RELS {{ getIndex(VAL) }} orDefault HostVal(0)) + => loadObject(rel2abs(RELS, VAL)) ... RELS @@ -371,6 +371,24 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly ``` +- rel2abs, rel2absMany: Convert relative handles to absolute handles + +```k + syntax HostVal ::= rel2abs(List, HostVal) [function, total, symbol(rel2abs)] + // ------------------------------------------------------------------------ + rule rel2abs(RELS, HV) => RELS {{ getIndex(HV) }} orDefault HV + requires isObject(HV) andBool isRelativeObjectHandle(HV) + rule rel2abs(_, HV) => HV + [owise] + + syntax List ::= rel2absMany(List, List) [function, total, symbol(rel2absMany)] + // -------------------------------------------------------------------------------- + rule rel2absMany(RELS, ListItem(HV) L) => ListItem(rel2abs(RELS, HV)) rel2absMany(RELS, L) + rule rel2absMany(_, L) => L + [owise] + +``` + ### Auxiliary functions ```k diff --git a/src/komet/kdist/soroban-semantics/host/map.md b/src/komet/kdist/soroban-semantics/host/map.md index 1f4fec8..aef32ca 100644 --- a/src/komet/kdist/soroban-semantics/host/map.md +++ b/src/komet/kdist/soroban-semantics/host/map.md @@ -91,7 +91,7 @@ The function returns a `HostVal` pointing to the new map object. ScMap( mapFromLists( KEYS, - Bytes2Vals(VALS_BS) + rel2absMany(RELS, Bytes2Vals(VALS_BS)) ) ) ) @@ -99,6 +99,7 @@ The function returns a `HostVal` pointing to the new map object. ... KEYS : VALS_BS : S => S + RELS requires size(KEYS) ==Int lengthBytes(VALS_BS) /Int 8 ``` diff --git a/src/komet/kdist/soroban-semantics/host/vector.md b/src/komet/kdist/soroban-semantics/host/vector.md index 8e77e56..47c0c74 100644 --- a/src/komet/kdist/soroban-semantics/host/vector.md +++ b/src/komet/kdist/soroban-semantics/host/vector.md @@ -76,8 +76,15 @@ module HOST-VECTOR U32(VALS_POS) : U32(LEN) : S => S rule [vecNewFromLinearMemoryAux]: - vecNewFromLinearMemoryAux => allocObject(ScVec(Bytes2Vals(BS))) ... + vecNewFromLinearMemoryAux + => allocObject( + ScVec( + rel2absMany(RELS, Bytes2Vals(BS)) + ) + ) ... + BS : S => S + RELS syntax Bytes ::= Vals2Bytes(List) [function, total] diff --git a/src/komet/scval.py b/src/komet/scval.py index 9e3b368..c10de2a 100644 --- a/src/komet/scval.py +++ b/src/komet/scval.py @@ -10,6 +10,9 @@ from pyk.prelude.utils import token from .kast.syntax import ( + account_id, + contract_id, + sc_address, sc_bool, sc_bytes, sc_i32, @@ -120,6 +123,30 @@ def to_kast(self) -> KInner: return sc_bytes(self.val) +@dataclass(frozen=True) +class AccountId: + val: bytes + + def to_kast(self) -> KInner: + return account_id(self.val) + + +@dataclass(frozen=True) +class ContractId: + val: bytes + + def to_kast(self) -> KInner: + return contract_id(self.val) + + +@dataclass(frozen=True) +class SCAddress(SCValue): + val: AccountId | ContractId + + def to_kast(self) -> KInner: + return sc_address(self.val.to_kast()) + + @dataclass(frozen=True) class SCVec(SCValue): val: tuple[SCValue] @@ -150,6 +177,7 @@ def to_kast(self) -> KInner: 'u256': 'SCU256Type', 'symbol': 'SCSymbolType', 'bytes': 'SCBytesType', + 'address': 'SCAddressType', 'vec': 'SCVecType', 'map': 'SCMapType', } @@ -330,6 +358,21 @@ def as_var(cls, name: str) -> tuple[KInner, tuple[KInner, ...]]: return KApply('SCVal:Bytes', [KVariable(name, KSort('Bytes'))]), () +@dataclass +class SCAddressType(SCMonomorphicType): + def strategy(self) -> strategies.SearchStrategy: + def target(p: bool, val: bytes) -> SCAddress: + if p: + return SCAddress(ContractId(val)) + return SCAddress(AccountId(val)) + + return strategies.builds(target, strategies.booleans(), strategies.binary(min_size=32, max_size=32)) + + @classmethod + def as_var(cls, name: str) -> tuple[KInner, tuple[KInner, ...]]: + return KApply('SCVal:Address', [KVariable(name, KSort('Address'))]), () + + @dataclass class SCVecType(SCType): element: SCType diff --git a/src/tests/integration/data/soroban/contracts/test_fxdao/src/lib.rs b/src/tests/integration/data/soroban/contracts/test_fxdao/src/lib.rs index 7bbcb10..b169265 100644 --- a/src/tests/integration/data/soroban/contracts/test_fxdao/src/lib.rs +++ b/src/tests/integration/data/soroban/contracts/test_fxdao/src/lib.rs @@ -70,6 +70,15 @@ impl TestFxDAOContract { true } + pub fn test_set_admin(env: Env, addr: Address) -> bool { + let fxdao_addr: Address = env.storage().instance().get(&FXDAO_KEY).unwrap(); + let client = VaultsContract::Client::new(&env, &fxdao_addr); + + client.set_admin(&addr); + + let core_state = client.get_core_state(); + core_state.admin == addr + } } mod test;