implement map_put

runtimeverification · Nov 12, 2024 · dd53694 · dd53694
1 parent 6dd693c
commit dd53694
Show file tree

Hide file tree

Showing 2 changed files with 75 additions and 0 deletions.
diff --git a/src/komet/kdist/soroban-semantics/host/map.md b/src/komet/kdist/soroban-semantics/host/map.md
@@ -29,6 +29,33 @@ module HOST-MAP
         <locals> .Map </locals>
 ```
 
+## map_put
+
+```k
+    rule [hostfun-map-put]:
+        <instrs> hostCall ( "m" , "0" , [ i64  i64  i64  .ValTypes ] -> [ i64  .ValTypes ] )
+              => pushStack(HostVal(VAL))
+              ~> loadObjectFull(HostVal(KEY))
+              ~> loadObject(HostVal(M))
+              ~> hostCallAux("m", "0")
+                 ...
+        </instrs>
+        <locals>
+          0 |-> < i64 > M
+          1 |-> < i64 > KEY
+          2 |-> < i64 > VAL
+        </locals>
+
+    rule [hostCallAux-map-put]:
+        <instrs> hostCallAux("m", "0")
+              => allocObject(ScMap( M [ KEY <- VAL ] ))
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <hostStack> ScMap(M) : KEY:ScVal : VAL:HostVal : S => S </hostStack>
+
+```
+
 ## map_get
 
 ```k

diff --git a/src/tests/integration/data/map.wast b/src/tests/integration/data/map.wast
@@ -140,4 +140,52 @@ callTx(
   )
 )
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; map_put
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+callTx(
+  Account(b"test-caller"),
+  Contract(b"test-sc"),
+  "put",
+  ListItem(ScMap(.Map)) ListItem(Symbol(str("foo"))) ListItem(U32(123456)),
+  ScMap(Symbol(str("foo")) |-> U32(123456))
+)
+
+callTx(
+  Account(b"test-caller"),
+  Contract(b"test-sc"),
+  "put",
+  ListItem(ScMap(
+    Symbol(str("bar")) |-> Symbol(str("456"))
+    Symbol(str("baz")) |-> U128(789)
+  ))
+  ListItem(Symbol(str("foo")))
+  ListItem(U32(123)),
+  ScMap(
+    Symbol(str("foo")) |-> U32(123)
+    Symbol(str("bar")) |-> Symbol(str("456"))
+    Symbol(str("baz")) |-> U128(789)
+  )
+)
+
+;; Overwrite
+callTx(
+  Account(b"test-caller"),
+  Contract(b"test-sc"),
+  "put",
+  ListItem(ScMap(
+    Symbol(str("foo")) |-> U32(1)
+    Symbol(str("bar")) |-> Symbol(str("456"))
+    Symbol(str("baz")) |-> U128(789)
+  ))
+  ListItem(Symbol(str("foo")))
+  ListItem(U32(123)),
+  ScMap(
+    Symbol(str("foo")) |-> U32(123)
+    Symbol(str("bar")) |-> Symbol(str("456"))
+    Symbol(str("baz")) |-> U128(789)
+  )
+)
+
 setExitCode(0)