Fix relative handles in containers

package/version

@@ -1 +1 @@
-0.1.33
+0.1.34

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. <[email protected]>",

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))
 

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]:
         <instrs> loadObject(VAL)
-              => loadObject(RELS {{ getIndex(VAL) }} orDefault HostVal(0))
+              => loadObject(rel2abs(RELS, VAL))
                  ...
         </instrs>
         <relativeObjects> RELS </relativeObjects>
@@ -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

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

@@ -91,14 +91,15 @@ The function returns a `HostVal` pointing to the new map object.
                     ScMap(
                       mapFromLists(
                         KEYS,
-                        Bytes2Vals(VALS_BS)
+                        rel2absMany(RELS, Bytes2Vals(VALS_BS))
                       )
                     )
                   )
               ~> returnHostVal
                  ...
         </instrs>
         <hostStack> KEYS : VALS_BS : S => S </hostStack>
+        <relativeObjects> RELS </relativeObjects>
       requires size(KEYS) ==Int lengthBytes(VALS_BS) /Int 8
 
 ```

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

@@ -76,8 +76,15 @@ module HOST-VECTOR
         <hostStack> U32(VALS_POS) : U32(LEN) : S => S </hostStack>
 
     rule [vecNewFromLinearMemoryAux]:
-        <instrs> vecNewFromLinearMemoryAux => allocObject(ScVec(Bytes2Vals(BS))) ... </instrs>
+        <instrs> vecNewFromLinearMemoryAux
+              => allocObject(
+                    ScVec(
+                      rel2absMany(RELS, Bytes2Vals(BS))
+                    )
+                  ) ...
+        </instrs>
         <hostStack> BS : S => S </hostStack>
+        <relativeObjects> RELS </relativeObjects>
 
 
     syntax Bytes ::= Vals2Bytes(List)    [function, total]

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

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;