implement map_del

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

Hide file tree

Showing 2 changed files with 51 additions and 0 deletions.
diff --git a/src/komet/kdist/soroban-semantics/host/map.md b/src/komet/kdist/soroban-semantics/host/map.md
@@ -60,6 +60,37 @@ module HOST-MAP
 
 ```
 
+## map_del
+
+```k
+    rule [hostfun-map-del]:
+        <instrs> hostCall ( "m" , "2" , [ i64  i64  .ValTypes ] -> [ i64  .ValTypes ] )
+              => loadObjectFull(HostVal(KEY))
+              ~> loadObject(HostVal(M))
+              ~> hostCallAux("m", "2")
+                 ...
+        </instrs>
+        <locals>
+          0 |-> < i64 > M
+          1 |-> < i64 > KEY
+        </locals>
+
+    rule [hostCallAux-map-del]:
+        <instrs> hostCallAux("m", "2")
+              => allocObject(ScMap( M [ KEY <- undef ] ))
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <hostStack> ScMap(M) : KEY:ScVal : S => S </hostStack>
+      requires KEY in_keys(M)
+
+    rule [hostCallAux-map-del-not-found]:
+        <instrs> hostCallAux("m", "2") => trap ... </instrs>
+        <hostStack> ScMap(M) : KEY:ScVal : S => S </hostStack>
+      requires notBool( KEY in_keys(M) )
+
+```
+
 ## map_len
 
 ```k

diff --git a/src/tests/integration/data/map.wast b/src/tests/integration/data/map.wast
@@ -120,4 +120,24 @@ callTx(
   U32(123)
 )
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; map_del
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+callTx(
+  Account(b"test-caller"),
+  Contract(b"test-sc"),
+  "del",
+  ListItem(ScMap(
+    Symbol(str("foo")) |-> U32(123)
+    Symbol(str("bar")) |-> Symbol(str("456"))
+    Symbol(str("baz")) |-> U128(789)
+  ))
+  ListItem(Symbol(str("foo"))),
+  ScMap(
+    Symbol(str("bar")) |-> Symbol(str("456"))
+    Symbol(str("baz")) |-> U128(789)
+  )
+)
+
 setExitCode(0)