Convert rel handles to abs when creating maps and vecs

runtimeverification · Sep 12, 2024 · 1d91bcd · 1d91bcd
1 parent ed78e76
commit 1d91bcd
Show file tree

Hide file tree

Showing 3 changed files with 29 additions and 3 deletions.
diff --git 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]:
         <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

diff --git a/src/komet/kdist/soroban-semantics/host/map.md b/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
 
 ```

diff --git 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
         <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]